Documentation

EValues.Mathlib.iSup

Lemmas about iSup and iInf #

source
theorem iSup₂_eq_sSup {α : Type u_1} {ι : Type u_2} [CompleteLattice ι] {P : α → Prop} {g : α → ι} :
⨆ (x : α), ⨆ (_ : P x), g x = sSup {y : ι | ∃ (x : α), P x ∧ y = g x}
source
theorem iSup₃_eq_sSup {α : Type u_1} {ι : Type u_2} [CompleteLattice ι] {P₁ P₂ : α → Prop} {g : α → ι} :
⨆ (x : α), ⨆ (_ : P₁ x), ⨆ (_ : P₂ x), g x = sSup {y : ι | ∃ (x : α), P₁ x ∧ P₂ x ∧ y = g x}
source
theorem iInf₂_eq_sInf {α : Type u_1} {ι : Type u_2} [CompleteLattice ι] {P : α → Prop} {g : α → ι} :
⨅ (x : α), ⨅ (_ : P x), g x = sInf {y : ι | ∃ (x : α), P x ∧ y = g x}
source
theorem iInf₃_eq_sInf {α : Type u_1} {ι : Type u_2} [CompleteLattice ι] {P₁ P₂ : α → Prop} {g : α → ι} :
⨅ (x : α), ⨅ (_ : P₁ x), ⨅ (_ : P₂ x), g x = sInf {y : ι | ∃ (x : α), P₁ x ∧ P₂ x ∧ y = g x}
source
theorem iInf₄_eq_sInf {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CompleteLattice ι] {P₁ : α → Prop} {P₂ : β → Prop} {g : α → β → ι} :
⨅ (x : α), ⨅ (y : β), ⨅ (_ : P₁ x), ⨅ (_ : P₂ y), g x y = sInf {z : ι | ∃ (x : α) (y : β), P₁ x ∧ P₂ y ∧ z = g x y}
source
theorem iSup₄_eq_sSup {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CompleteLattice ι] {P₁ : α → Prop} {P₂ : β → Prop} {g : α → β → ι} :
⨆ (x : α), ⨆ (y : β), ⨆ (_ : P₁ x), ⨆ (_ : P₂ y), g x y = sSup {z : ι | ∃ (x : α) (y : β), P₁ x ∧ P₂ y ∧ z = g x y}
source
theorem sInf_add' {α : Type u_1} [AddCommMagma α] [Sub α] [CompleteLattice α] [OrderedSub α] {s t : Set α} :
sInf (s + t) = sInf s + sInf t
source
theorem iInf₂_add {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMagma ι] [Sub ι] [CompleteLattice ι] [OrderedSub ι] {P₁ : α → Prop} {P₂ : β → Prop} {f : α → ι} {g : β → ι} :
(⨅ (x : α), ⨅ (_ : P₁ x), f x) + ⨅ (y : β), ⨅ (_ : P₂ y), g y = ⨅ (x : α), ⨅ (y : β), ⨅ (_ : P₁ x), ⨅ (_ : P₂ y), f x + g y
source
theorem exists_iSup₂_EReal_add {α : Type u_1} {β : Type u_2} {P₁ : α → Prop} {P₂ : β → Prop} {f : α → EReal} {g : β → EReal} {x : α} (hx : P₁ x) {y : β} (hy : P₂ y) (hx_sup : f x = ⨆ (x : α), ⨆ (_ : P₁ x), f x) (hy_sup : g y = ⨆ (y : β), ⨆ (_ : P₂ y), g y) :
(⨆ (x : α), ⨆ (_ : P₁ x), f x) + ⨆ (y : β), ⨆ (_ : P₂ y), g y = ⨆ (x : α), ⨆ (y : β), ⨆ (_ : P₁ x), ⨆ (_ : P₂ y), f x + g y