# Theory of complete lattices #

This file contains basic results on complete lattices.

## Naming conventions #

In lemma names,

- `sSup` is called `sSup`
- `sInf` is called `sInf`
- `⨆ i, s i` is called `iSup`
- `⨅ i, s i` is called `iInf`
- `⨆ i j, s i j` is called `iSup₂`. This is an `iSup` inside an `iSup`.
- `⨅ i j, s i j` is called `iInf₂`. This is an `iInf` inside an `iInf`.
- `⨆ i ∈ s, t i` is called `biSup` for "bounded `iSup`". This is the special case of `iSup₂` where `j : i ∈ s`.
- `⨅ i ∈ s, t i` is called `biInf` for "bounded `iInf`". This is the special case of `iInf₂` where `j : i ∈ s`.

## Notation #

- `⨆ i, f i` : `iSup f`, the supremum of the range of `f`;
- `⨅ i, f i` : `iInf f`, the infimum of the range of `f`.

source
@[simp]
theorem iSup_ulift {α : Type u_1} {ι : Type u_8} [SupSet α] (f : ULift.{u_9, u_8} ι → α) :
⨆ (i : ULift.{u_9, u_8} ι), f i = ⨆ (i : ι), f { down := i }
source
@[simp]
theorem iInf_ulift {α : Type u_1} {ι : Type u_8} [InfSet α] (f : ULift.{u_9, u_8} ι → α) :
⨅ (i : ULift.{u_9, u_8} ι), f i = ⨅ (i : ι), f { down := i }
source
theorem sSup_le_sSup_of_isCofinalFor {α : Type u_1} [CompleteSemilatticeSup α] {s t : Set α} (h : IsCofinalFor s t) :
sSup s ≤ sSup t
source
@[deprecated "use `sSup_le_sSup_of_isCofinalFor` instead" (since := "2025-07-14")]
theorem sSup_le_sSup_of_forall_exists_le {α : Type u_1} [CompleteSemilatticeSup α] {s t : Set α} (h : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) :
sSup s ≤ sSup t
source
@[simp]
theorem sSup_singleton {α : Type u_1} [CompleteSemilatticeSup α] {a : α} :
sSup {a} = a
source
theorem sInf_le_sInf_of_isCoinitialFor {α : Type u_1} [CompleteSemilatticeInf α] {s t : Set α} (h : IsCoinitialFor s t) :
sInf t ≤ sInf s
source
@[deprecated "use `sInf_le_sInf_of_isCoinitialFor` instead" (since := "2025-07-14")]
theorem sInf_le_sInf_of_forall_exists_le {α : Type u_1} [CompleteSemilatticeInf α] {s t : Set α} (h : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) :
sInf t ≤ sInf s
source
@[simp]
theorem sInf_singleton {α : Type u_1} [CompleteSemilatticeInf α] {a : α} :
sInf {a} = a
source
theorem sInf_le_sSup {α : Type u_1} [CompleteLattice α] {s : Set α} (hs : s.Nonempty) :
sInf s ≤ sSup s
source
theorem sSup_union {α : Type u_1} [CompleteLattice α] {s t : Set α} :
sSup (s ∪ t) = sSup s ⊔ sSup t
source
theorem sInf_union {α : Type u_1} [CompleteLattice α] {s t : Set α} :
sInf (s ∪ t) = sInf s ⊓ sInf t
source
theorem sSup_inter_le {α : Type u_1} [CompleteLattice α] {s t : Set α} :
sSup (s ∩ t) ≤ sSup s ⊓ sSup t
source
theorem le_sInf_inter {α : Type u_1} [CompleteLattice α] {s t : Set α} :
sInf s ⊔ sInf t ≤ sInf (s ∩ t)
source
@[simp]
theorem sSup_empty {α : Type u_1} [CompleteLattice α] :
sSup ∅ = ⊥
source
@[simp]
theorem sInf_empty {α : Type u_1} [CompleteLattice α] :
sInf ∅ = ⊤
source
@[simp]
theorem sSup_univ {α : Type u_1} [CompleteLattice α] :
sSup Set.univ = ⊤
source
@[simp]
theorem sInf_univ {α : Type u_1} [CompleteLattice α] :
sInf Set.univ = ⊥
source
@[simp]
theorem sSup_insert {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} :
sSup (insert a s) = a ⊔ sSup s
source
@[simp]
theorem sInf_insert {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} :
sInf (insert a s) = a ⊓ sInf s
source
theorem sSup_le_sSup_of_subset_insert_bot {α : Type u_1} [CompleteLattice α] {s t : Set α} (h : s ⊆ insert ⊥ t) :
sSup s ≤ sSup t
source
theorem sInf_le_sInf_of_subset_insert_top {α : Type u_1} [CompleteLattice α] {s t : Set α} (h : s ⊆ insert ⊤ t) :
sInf t ≤ sInf s
source
@[simp]
theorem sSup_diff_singleton_bot {α : Type u_1} [CompleteLattice α] (s : Set α) :
sSup (s \ {⊥}) = sSup s
source
@[simp]
theorem sInf_diff_singleton_top {α : Type u_1} [CompleteLattice α] (s : Set α) :
sInf (s \ {⊤}) = sInf s
source
theorem sSup_pair {α : Type u_1} [CompleteLattice α] {a b : α} :
sSup {a, b} = a ⊔ b
source
theorem sInf_pair {α : Type u_1} [CompleteLattice α] {a b : α} :
sInf {a, b} = a ⊓ b
source
@[simp]
theorem sSup_eq_bot {α : Type u_1} [CompleteLattice α] {s : Set α} :
sSup s = ⊥ ↔ ∀ a ∈ s, a = ⊥
source
@[simp]
theorem sInf_eq_top {α : Type u_1} [CompleteLattice α] {s : Set α} :
sInf s = ⊤ ↔ ∀ a ∈ s, a = ⊤
source
theorem sSup_eq_bot' {α : Type u_1} [CompleteLattice α] {s : Set α} :
sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥}
source
theorem eq_singleton_bot_of_sSup_eq_bot_of_nonempty {α : Type u_1} [CompleteLattice α] {s : Set α} (h_sup : sSup s = ⊥) (hne : s.Nonempty) :
s = {⊥}
source
theorem eq_singleton_top_of_sInf_eq_top_of_nonempty {α : Type u_1} [CompleteLattice α] {s : Set α} :
sInf s = ⊤ → s.Nonempty → s = {⊤}
source
theorem sSup_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} [CompleteLattice α] {s : Set α} {b : α} (h₁ : ∀ a ∈ s, a ≤ b) (h₂ : ∀ w < b, ∃ a ∈ s, w < a) :
sSup s = b

Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that `b` is larger than all elements of `s`, and that this is not the case of any `w < b`. See `csSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in conditionally complete lattices.

source
theorem sInf_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} [CompleteLattice α] {s : Set α} {b : α} :
(∀ a ∈ s, b ≤ a) → (∀ (w : α), b < w → ∃ a ∈ s, a < w) → sInf s = b

Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b` is smaller than all elements of `s`, and that this is not the case of any `w > b`. See `csInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in conditionally complete lattices.

source
theorem sSup_range {α : Type u_1} {ι : Sort u_4} [SupSet α] {f : ι → α} :
sSup (Set.range f) = iSup f
source
theorem sSup_eq_iSup' {α : Type u_1} [SupSet α] (s : Set α) :
sSup s = ⨆ (a : ↑s), ↑a
source
theorem iSup_congr {α : Type u_1} {ι : Sort u_4} [SupSet α] {f g : ι → α} (h : ∀ (i : ι), f i = g i) :
⨆ (i : ι), f i = ⨆ (i : ι), g i
source
theorem biSup_congr {α : Type u_1} {ι : Sort u_4} [SupSet α] {f g : ι → α} {p : ι → Prop} (h : ∀ (i : ι), p i → f i = g i) :
⨆ (i : ι), ⨆ (_ : p i), f i = ⨆ (i : ι), ⨆ (_ : p i), g i
source
theorem biSup_congr' {α : Type u_1} {ι : Sort u_4} [SupSet α] {p : ι → Prop} {f g : (i : ι) → p i → α} (h : ∀ (i : ι) (hi : p i), f i hi = g i hi) :
⨆ (i : ι), ⨆ (hi : p i), f i hi = ⨆ (i : ι), ⨆ (hi : p i), g i hi
source
theorem Function.Surjective.iSup_comp {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [SupSet α] {f : ι → ι'} (hf : Surjective f) (g : ι' → α) :
⨆ (x : ι), g (f x) = ⨆ (y : ι'), g y
source
theorem Equiv.iSup_comp {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [SupSet α] {g : ι' → α} (e : ι ≃ ι') :
⨆ (x : ι), g (e x) = ⨆ (y : ι'), g y
source
theorem Function.Surjective.iSup_congr {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [SupSet α] {f : ι → α} {g : ι' → α} (h : ι → ι') (h1 : Surjective h) (h2 : ∀ (x : ι), g (h x) = f x) :
⨆ (x : ι), f x = ⨆ (y : ι'), g y
source
theorem Equiv.iSup_congr {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [SupSet α] {f : ι → α} {g : ι' → α} (e : ι ≃ ι') (h : ∀ (x : ι), g (e x) = f x) :
⨆ (x : ι), f x = ⨆ (y : ι'), g y
source
theorem iSup_congr_Prop {α : Type u_1} [SupSet α] {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q) (f : ∀ (x : q), f₁ ⋯ = f₂ x) :
iSup f₁ = iSup f₂
source
theorem iSup_plift_up {α : Type u_1} {ι : Sort u_4} [SupSet α] (f : PLift ι → α) :
⨆ (i : ι), f { down := i } = ⨆ (i : PLift ι), f i
source
theorem iSup_plift_down {α : Type u_1} {ι : Sort u_4} [SupSet α] (f : ι → α) :
⨆ (i : PLift ι), f i.down = ⨆ (i : ι), f i
source
theorem iSup_range' {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [SupSet α] (g : β → α) (f : ι → β) :
⨆ (b : ↑(Set.range f)), g ↑b = ⨆ (i : ι), g (f i)
source
theorem sSup_image' {α : Type u_1} {β : Type u_2} [SupSet α] {s : Set β} {f : β → α} :
sSup (f '' s) = ⨆ (a : ↑s), f ↑a
source
theorem sInf_range {α : Type u_1} {ι : Sort u_4} [InfSet α] {f : ι → α} :
sInf (Set.range f) = iInf f
source
theorem sInf_eq_iInf' {α : Type u_1} [InfSet α] (s : Set α) :
sInf s = ⨅ (a : ↑s), ↑a
source
theorem iInf_congr {α : Type u_1} {ι : Sort u_4} [InfSet α] {f g : ι → α} (h : ∀ (i : ι), f i = g i) :
⨅ (i : ι), f i = ⨅ (i : ι), g i
source
theorem biInf_congr {α : Type u_1} {ι : Sort u_4} [InfSet α] {f g : ι → α} {p : ι → Prop} (h : ∀ (i : ι), p i → f i = g i) :
⨅ (i : ι), ⨅ (_ : p i), f i = ⨅ (i : ι), ⨅ (_ : p i), g i
source
theorem biInf_congr' {α : Type u_1} {ι : Sort u_4} [InfSet α] {p : ι → Prop} {f g : (i : ι) → p i → α} (h : ∀ (i : ι) (hi : p i), f i hi = g i hi) :
⨅ (i : ι), ⨅ (hi : p i), f i hi = ⨅ (i : ι), ⨅ (hi : p i), g i hi
source
theorem Function.Surjective.iInf_comp {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [InfSet α] {f : ι → ι'} (hf : Surjective f) (g : ι' → α) :
⨅ (x : ι), g (f x) = ⨅ (y : ι'), g y
source
theorem Equiv.iInf_comp {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [InfSet α] {g : ι' → α} (e : ι ≃ ι') :
⨅ (x : ι), g (e x) = ⨅ (y : ι'), g y
source
theorem Function.Surjective.iInf_congr {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [InfSet α] {f : ι → α} {g : ι' → α} (h : ι → ι') (h1 : Surjective h) (h2 : ∀ (x : ι), g (h x) = f x) :
⨅ (x : ι), f x = ⨅ (y : ι'), g y
source
theorem Equiv.iInf_congr {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [InfSet α] {f : ι → α} {g : ι' → α} (e : ι ≃ ι') (h : ∀ (x : ι), g (e x) = f x) :
⨅ (x : ι), f x = ⨅ (y : ι'), g y
source
theorem iInf_congr_Prop {α : Type u_1} [InfSet α] {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q) (f : ∀ (x : q), f₁ ⋯ = f₂ x) :
iInf f₁ = iInf f₂
source
theorem iInf_plift_up {α : Type u_1} {ι : Sort u_4} [InfSet α] (f : PLift ι → α) :
⨅ (i : ι), f { down := i } = ⨅ (i : PLift ι), f i
source
theorem iInf_plift_down {α : Type u_1} {ι : Sort u_4} [InfSet α] (f : ι → α) :
⨅ (i : PLift ι), f i.down = ⨅ (i : ι), f i
source
theorem iInf_range' {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [InfSet α] (g : β → α) (f : ι → β) :
⨅ (b : ↑(Set.range f)), g ↑b = ⨅ (i : ι), g (f i)
source
theorem sInf_image' {α : Type u_1} {β : Type u_2} [InfSet α] {s : Set β} {f : β → α} :
sInf (f '' s) = ⨅ (a : ↑s), f ↑a
source
theorem le_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ι → α) (i : ι) :
f i ≤ iSup f
source
theorem iInf_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ι → α) (i : ι) :
iInf f ≤ f i
source
theorem iInf_le_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} [Nonempty ι] :
⨅ (i : ι), f i ≤ ⨆ (i : ι), f i
source
theorem isLUB_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} :
IsLUB (Set.range f) (⨆ (j : ι), f j)
source
theorem isGLB_iInf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} :
IsGLB (Set.range f) (⨅ (j : ι), f j)
source
theorem IsLUB.iSup_eq {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {a : α} (h : IsLUB (Set.range f) a) :
⨆ (j : ι), f j = a
source
theorem IsGLB.iInf_eq {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {a : α} (h : IsGLB (Set.range f) a) :
⨅ (j : ι), f j = a
source
theorem le_iSup_of_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {a : α} (i : ι) (h : a ≤ f i) :
a ≤ iSup f
source
theorem iInf_le_of_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {a : α} (i : ι) (h : f i ≤ a) :
iInf f ≤ a
source
theorem le_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] {f : (i : ι) → κ i → α} (i : ι) (j : κ i) :
f i j ≤ ⨆ (i : ι), ⨆ (j : κ i), f i j
source
theorem iInf₂_le {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] {f : (i : ι) → κ i → α} (i : ι) (j : κ i) :
⨅ (i : ι), ⨅ (j : κ i), f i j ≤ f i j
source
theorem le_iSup₂_of_le {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (i : ι) (j : κ i) (h : a ≤ f i j) :
a ≤ ⨆ (i : ι), ⨆ (j : κ i), f i j
source
theorem iInf₂_le_of_le {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (i : ι) (j : κ i) (h : f i j ≤ a) :
⨅ (i : ι), ⨅ (j : κ i), f i j ≤ a
source
theorem iSup_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {a : α} (h : ∀ (i : ι), f i ≤ a) :
iSup f ≤ a
source
theorem le_iInf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {a : α} (h : ∀ (i : ι), a ≤ f i) :
a ≤ iInf f
source
theorem iSup₂_le {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (h : ∀ (i : ι) (j : κ i), f i j ≤ a) :
⨆ (i : ι), ⨆ (j : κ i), f i j ≤ a
source
theorem le_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (h : ∀ (i : ι) (j : κ i), a ≤ f i j) :
a ≤ ⨅ (i : ι), ⨅ (j : κ i), f i j
source
theorem iSup₂_le_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (κ : ι → Sort u_8) (f : ι → α) :
⨆ (i : ι), ⨆ (x : κ i), f i ≤ ⨆ (i : ι), f i
source
theorem iInf_le_iInf₂ {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (κ : ι → Sort u_8) (f : ι → α) :
⨅ (i : ι), f i ≤ ⨅ (i : ι), ⨅ (x : κ i), f i
source
theorem iSup_mono {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f g : ι → α} (h : ∀ (i : ι), f i ≤ g i) :
iSup f ≤ iSup g
source
theorem iInf_mono {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f g : ι → α} (h : ∀ (i : ι), f i ≤ g i) :
iInf f ≤ iInf g
source
theorem iSup₂_mono {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] {f g : (i : ι) → κ i → α} (h : ∀ (i : ι) (j : κ i), f i j ≤ g i j) :
⨆ (i : ι), ⨆ (j : κ i), f i j ≤ ⨆ (i : ι), ⨆ (j : κ i), g i j
source
theorem iInf₂_mono {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] {f g : (i : ι) → κ i → α} (h : ∀ (i : ι) (j : κ i), f i j ≤ g i j) :
⨅ (i : ι), ⨅ (j : κ i), f i j ≤ ⨅ (i : ι), ⨅ (j : κ i), g i j
source
theorem iSup_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] {f : ι → α} {g : ι' → α} (h : ∀ (i : ι), ∃ (i' : ι'), f i ≤ g i') :
iSup f ≤ iSup g
source
theorem iInf_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] {f : ι → α} {g : ι' → α} (h : ∀ (i' : ι'), ∃ (i : ι), f i ≤ g i') :
iInf f ≤ iInf g
source
theorem iSup₂_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {κ : ι → Sort u_6} {κ' : ι' → Sort u_7} [CompleteLattice α] {f : (i : ι) → κ i → α} {g : (i' : ι') → κ' i' → α} (h : ∀ (i : ι) (j : κ i), ∃ (i' : ι') (j' : κ' i'), f i j ≤ g i' j') :
⨆ (i : ι), ⨆ (j : κ i), f i j ≤ ⨆ (i : ι'), ⨆ (j : κ' i), g i j
source
theorem iInf₂_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {κ : ι → Sort u_6} {κ' : ι' → Sort u_7} [CompleteLattice α] {f : (i : ι) → κ i → α} {g : (i' : ι') → κ' i' → α} (h : ∀ (i : ι') (j : κ' i), ∃ (i' : ι) (j' : κ i'), f i' j' ≤ g i j) :
⨅ (i : ι), ⨅ (j : κ i), f i j ≤ ⨅ (i : ι'), ⨅ (j : κ' i), g i j
source
theorem iSup_const_mono {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] {a : α} (h : ι → ι') :
⨆ (x : ι), a ≤ ⨆ (x : ι'), a
source
theorem iInf_const_mono {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] {a : α} (h : ι' → ι) :
⨅ (x : ι), a ≤ ⨅ (x : ι'), a
source
theorem iSup_iInf_le_iInf_iSup {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] (f : ι → ι' → α) :
⨆ (i : ι), ⨅ (j : ι'), f i j ≤ ⨅ (j : ι'), ⨆ (i : ι), f i j
source
theorem biSup_mono {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {p q : ι → Prop} (hpq : ∀ (i : ι), p i → q i) :
⨆ (i : ι), ⨆ (_ : p i), f i ≤ ⨆ (i : ι), ⨆ (_ : q i), f i
source
theorem biInf_mono {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {p q : ι → Prop} (hpq : ∀ (i : ι), p i → q i) :
⨅ (i : ι), ⨅ (_ : q i), f i ≤ ⨅ (i : ι), ⨅ (_ : p i), f i
source
@[simp]
theorem iSup_le_iff {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {a : α} :
iSup f ≤ a ↔ ∀ (i : ι), f i ≤ a
source
@[simp]
theorem le_iInf_iff {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {a : α} :
a ≤ iInf f ↔ ∀ (i : ι), a ≤ f i
source
theorem iSup₂_le_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} :
⨆ (i : ι), ⨆ (j : κ i), f i j ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a
source
theorem le_iInf₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} :
a ≤ ⨅ (i : ι), ⨅ (j : κ i), f i j ↔ ∀ (i : ι) (j : κ i), a ≤ f i j
source
theorem iSup_lt_iff {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {a : α} :
iSup f < a ↔ ∃ b < a, ∀ (i : ι), f i ≤ b
source
theorem lt_iInf_iff {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {a : α} :
a < iInf f ↔ ∃ (b : α), a < b ∧ ∀ (i : ι), b ≤ f i
source
theorem sSup_eq_iSup {α : Type u_1} [CompleteLattice α] {s : Set α} :
sSup s = ⨆ a ∈ s, a
source
theorem sInf_eq_iInf {α : Type u_1} [CompleteLattice α] {s : Set α} :
sInf s = ⨅ a ∈ s, a
source
theorem sSup_lowerBounds_eq_sInf {α : Type u_1} [CompleteLattice α] (s : Set α) :
sSup (lowerBounds s) = sInf s
source
theorem sInf_upperBounds_eq_csSup {α : Type u_1} [CompleteLattice α] (s : Set α) :
sInf (upperBounds s) = sSup s
source
theorem Monotone.le_map_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {s : ι → α} [CompleteLattice β] {f : α → β} (hf : Monotone f) :
⨆ (i : ι), f (s i) ≤ f (iSup s)
source
theorem Antitone.le_map_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {s : ι → α} [CompleteLattice β] {f : α → β} (hf : Antitone f) :
⨆ (i : ι), f (s i) ≤ f (iInf s)
source
theorem Monotone.le_map_iSup₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : Monotone f) (s : (i : ι) → κ i → α) :
⨆ (i : ι), ⨆ (j : κ i), f (s i j) ≤ f (⨆ (i : ι), ⨆ (j : κ i), s i j)
source
theorem Antitone.le_map_iInf₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : Antitone f) (s : (i : ι) → κ i → α) :
⨆ (i : ι), ⨆ (j : κ i), f (s i j) ≤ f (⨅ (i : ι), ⨅ (j : κ i), s i j)
source
theorem Monotone.le_map_sSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) :
⨆ a ∈ s, f a ≤ f (sSup s)
source
theorem Antitone.le_map_sInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : α → β} (hf : Antitone f) :
⨆ a ∈ s, f a ≤ f (sInf s)
source
theorem OrderIso.map_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (x : ι → α) :
f (⨆ (i : ι), x i) = ⨆ (i : ι), f (x i)
source
theorem OrderIso.map_iSup₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (x : (i : ι) → κ i → α) :
f (⨆ (i : ι), ⨆ (j : κ i), x i j) = ⨆ (i : ι), ⨆ (j : κ i), f (x i j)
source
theorem OrderIso.map_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (x : ι → α) :
f (⨅ (i : ι), x i) = ⨅ (i : ι), f (x i)
source
theorem OrderIso.map_iInf₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (x : (i : ι) → κ i → α) :
f (⨅ (i : ι), ⨅ (j : κ i), x i j) = ⨅ (i : ι), ⨅ (j : κ i), f (x i j)
source
theorem OrderIso.map_sSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (s : Set α) :
f (sSup s) = ⨆ a ∈ s, f a
source
theorem OrderIso.map_sInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (s : Set α) :
f (sInf s) = ⨅ a ∈ s, f a
source
theorem iSup_comp_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {ι' : Sort u_8} (f : ι' → α) (g : ι → ι') :
⨆ (x : ι), f (g x) ≤ ⨆ (y : ι'), f y
source
theorem le_iInf_comp {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {ι' : Sort u_8} (f : ι' → α) (g : ι → ι') :
⨅ (y : ι'), f y ≤ ⨅ (x : ι), f (g x)
source
theorem Monotone.iSup_comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] [Preorder β] {f : β → α} (hf : Monotone f) {s : ι → β} (hs : ∀ (x : β), ∃ (i : ι), x ≤ s i) :
⨆ (x : ι), f (s x) = ⨆ (y : β), f y
source
theorem Monotone.iInf_comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] [Preorder β] {f : β → α} (hf : Monotone f) {s : ι → β} (hs : ∀ (x : β), ∃ (i : ι), s i ≤ x) :
⨅ (x : ι), f (s x) = ⨅ (y : β), f y
source
theorem Antitone.map_iSup_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {s : ι → α} [CompleteLattice β] {f : α → β} (hf : Antitone f) :
f (iSup s) ≤ ⨅ (i : ι), f (s i)
source
theorem Monotone.map_iInf_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {s : ι → α} [CompleteLattice β] {f : α → β} (hf : Monotone f) :
f (iInf s) ≤ ⨅ (i : ι), f (s i)
source
theorem Antitone.map_iSup₂_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : Antitone f) (s : (i : ι) → κ i → α) :
f (⨆ (i : ι), ⨆ (j : κ i), s i j) ≤ ⨅ (i : ι), ⨅ (j : κ i), f (s i j)
source
theorem Monotone.map_iInf₂_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : Monotone f) (s : (i : ι) → κ i → α) :
f (⨅ (i : ι), ⨅ (j : κ i), s i j) ≤ ⨅ (i : ι), ⨅ (j : κ i), f (s i j)
source
theorem Antitone.map_sSup_le {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : α → β} (hf : Antitone f) :
f (sSup s) ≤ ⨅ a ∈ s, f a
source
theorem Monotone.map_sInf_le {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) :
f (sInf s) ≤ ⨅ a ∈ s, f a
source
theorem iSup_const_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {a : α} :
⨆ (x : ι), a ≤ a
source
theorem le_iInf_const {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {a : α} :
a ≤ ⨅ (x : ι), a
source
theorem iSup_const {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {a : α} [Nonempty ι] :
⨆ (x : ι), a = a
source
theorem iInf_const {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {a : α} [Nonempty ι] :
⨅ (x : ι), a = a
source
theorem iSup_unique {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [Unique ι] (f : ι → α) :
⨆ (i : ι), f i = f default
source
theorem iInf_unique {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [Unique ι] (f : ι → α) :
⨅ (i : ι), f i = f default
source
@[simp]
theorem iSup_bot {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] :
⨆ (x : ι), ⊥ = ⊥
source
@[simp]
theorem iInf_top {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] :
⨅ (x : ι), ⊤ = ⊤
source
@[simp]
theorem iSup_eq_bot {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {s : ι → α} :
iSup s = ⊥ ↔ ∀ (i : ι), s i = ⊥
source
@[simp]
theorem iInf_eq_top {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {s : ι → α} :
iInf s = ⊤ ↔ ∀ (i : ι), s i = ⊤
source
@[simp]
theorem bot_lt_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {s : ι → α} :
⊥ < ⨆ (i : ι), s i ↔ ∃ (i : ι), ⊥ < s i
source
@[simp]
theorem iInf_lt_top {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {s : ι → α} :
⨅ (i : ι), s i < ⊤ ↔ ∃ (i : ι), s i < ⊤
source
theorem iSup₂_eq_bot {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] {f : (i : ι) → κ i → α} :
⨆ (i : ι), ⨆ (j : κ i), f i j = ⊥ ↔ ∀ (i : ι) (j : κ i), f i j = ⊥
source
theorem iInf₂_eq_top {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLattice α] {f : (i : ι) → κ i → α} :
⨅ (i : ι), ⨅ (j : κ i), f i j = ⊤ ↔ ∀ (i : ι) (j : κ i), f i j = ⊤
source
@[simp]
theorem iSup_pos {α : Type u_1} [CompleteLattice α] {p : Prop} {f : p → α} (hp : p) :
⨆ (h : p), f h = f hp
source
@[simp]
theorem iInf_pos {α : Type u_1} [CompleteLattice α] {p : Prop} {f : p → α} (hp : p) :
⨅ (h : p), f h = f hp
source
@[simp]
theorem iSup_neg {α : Type u_1} [CompleteLattice α] {p : Prop} {f : p → α} (hp : ¬p) :
⨆ (h : p), f h = ⊥
source
@[simp]
theorem iInf_neg {α : Type u_1} [CompleteLattice α] {p : Prop} {f : p → α} (hp : ¬p) :
⨅ (h : p), f h = ⊤
source
theorem iSup_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {b : α} {f : ι → α} (h₁ : ∀ (i : ι), f i ≤ b) (h₂ : ∀ w < b, ∃ (i : ι), w < f i) :
⨆ (i : ι), f i = b

Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b` is larger than `f i` for all `i`, and that this is not the case of any `w<b`. See `ciSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in conditionally complete lattices.

source
theorem iInf_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {b : α} :
(∀ (i : ι), b ≤ f i) → (∀ (w : α), b < w → ∃ (i : ι), f i < w) → ⨅ (i : ι), f i = b

Introduction rule to prove that `b` is the infimum of `f`: it suffices to check that `b` is smaller than `f i` for all `i`, and that this is not the case of any `w>b`. See `ciInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in conditionally complete lattices.

source
theorem iSup_eq_dif {α : Type u_1} [CompleteLattice α] {p : Prop} [Decidable p] (a : p → α) :
⨆ (h : p), a h = if h : p then a h else ⊥
source
theorem iSup_eq_if {α : Type u_1} [CompleteLattice α] {p : Prop} [Decidable p] (a : α) :
⨆ (_ : p), a = if p then a else ⊥
source
theorem iInf_eq_dif {α : Type u_1} [CompleteLattice α] {p : Prop} [Decidable p] (a : p → α) :
⨅ (h : p), a h = if h : p then a h else ⊤
source
theorem iInf_eq_if {α : Type u_1} [CompleteLattice α] {p : Prop} [Decidable p] (a : α) :
⨅ (_ : p), a = if p then a else ⊤
source
theorem iSup_comm {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] {f : ι → ι' → α} :
⨆ (i : ι), ⨆ (j : ι'), f i j = ⨆ (j : ι'), ⨆ (i : ι), f i j
source
theorem iInf_comm {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] {f : ι → ι' → α} :
⨅ (i : ι), ⨅ (j : ι'), f i j = ⨅ (j : ι'), ⨅ (i : ι), f i j
source
theorem iSup₂_comm {α : Type u_1} [CompleteLattice α] {ι₁ : Sort u_8} {ι₂ : Sort u_9} {κ₁ : ι₁ → Sort u_10} {κ₂ : ι₂ → Sort u_11} (f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α) :
⨆ (i₁ : ι₁), ⨆ (j₁ : κ₁ i₁), ⨆ (i₂ : ι₂), ⨆ (j₂ : κ₂ i₂), f i₁ j₁ i₂ j₂ = ⨆ (i₂ : ι₂), ⨆ (j₂ : κ₂ i₂), ⨆ (i₁ : ι₁), ⨆ (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂
source
theorem iInf₂_comm {α : Type u_1} [CompleteLattice α] {ι₁ : Sort u_8} {ι₂ : Sort u_9} {κ₁ : ι₁ → Sort u_10} {κ₂ : ι₂ → Sort u_11} (f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α) :
⨅ (i₁ : ι₁), ⨅ (j₁ : κ₁ i₁), ⨅ (i₂ : ι₂), ⨅ (j₂ : κ₂ i₂), f i₁ j₁ i₂ j₂ = ⨅ (i₂ : ι₂), ⨅ (j₂ : κ₂ i₂), ⨅ (i₁ : ι₁), ⨅ (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂
source
@[simp]
theorem iSup_iSup_eq_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {b : β} {f : (x : β) → x = b → α} :
⨆ (x : β), ⨆ (h : x = b), f x h = f b ⋯
source
@[simp]
theorem iInf_iInf_eq_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {b : β} {f : (x : β) → x = b → α} :
⨅ (x : β), ⨅ (h : x = b), f x h = f b ⋯
source
@[simp]
theorem iSup_iSup_eq_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {b : β} {f : (x : β) → b = x → α} :
⨆ (x : β), ⨆ (h : b = x), f x h = f b ⋯
source
@[simp]
theorem iInf_iInf_eq_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {b : β} {f : (x : β) → b = x → α} :
⨅ (x : β), ⨅ (h : b = x), f x h = f b ⋯
source
theorem iSup_subtype {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ι → Prop} {f : Subtype p → α} :
iSup f = ⨆ (i : ι), ⨆ (h : p i), f ⟨i, h⟩
source
theorem iInf_subtype {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ι → Prop} {f : Subtype p → α} :
iInf f = ⨅ (i : ι), ⨅ (h : p i), f ⟨i, h⟩
source
theorem iSup_subtype' {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} :
⨆ (i : ι), ⨆ (h : p i), f i h = ⨆ (x : Subtype p), f ↑x ⋯
source
theorem iInf_subtype' {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} :
⨅ (i : ι), ⨅ (h : p i), f i h = ⨅ (x : Subtype p), f ↑x ⋯
source
theorem iSup_subtype'' {α : Type u_1} [CompleteLattice α] {ι : Type u_8} (s : Set ι) (f : ι → α) :
⨆ (i : ↑s), f ↑i = ⨆ t ∈ s, f t
source
theorem iInf_subtype'' {α : Type u_1} [CompleteLattice α] {ι : Type u_8} (s : Set ι) (f : ι → α) :
⨅ (i : ↑s), f ↑i = ⨅ t ∈ s, f t
source
theorem biSup_const {α : Type u_1} {β : Type u_2} [CompleteLattice α] {a : α} {s : Set β} (hs : s.Nonempty) :
⨆ i ∈ s, a = a
source
theorem biInf_const {α : Type u_1} {β : Type u_2} [CompleteLattice α] {a : α} {s : Set β} (hs : s.Nonempty) :
⨅ i ∈ s, a = a
source
theorem iSup_sup_eq {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f g : ι → α} :
⨆ (x : ι), f x ⊔ g x = (⨆ (x : ι), f x) ⊔ ⨆ (x : ι), g x
source
theorem iInf_inf_eq {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f g : ι → α} :
⨅ (x : ι), f x ⊓ g x = (⨅ (x : ι), f x) ⊓ ⨅ (x : ι), g x
source
theorem Equiv.biSup_comp {α : Type u_1} [CompleteLattice α] {ι : Type u_8} {ι' : Type u_9} {g : ι' → α} (e : ι ≃ ι') (s : Set ι') :
⨆ i ∈ ⇑e.symm '' s, g (e i) = ⨆ i ∈ s, g i
source
theorem Equiv.biInf_comp {α : Type u_1} [CompleteLattice α] {ι : Type u_8} {ι' : Type u_9} {g : ι' → α} (e : ι ≃ ι') (s : Set ι') :
⨅ i ∈ ⇑e.symm '' s, g (e i) = ⨅ i ∈ s, g i
source
theorem biInf_le {α : Type u_1} [CompleteLattice α] {ι : Type u_8} {s : Set ι} (f : ι → α) {i : ι} (hi : i ∈ s) :
⨅ i ∈ s, f i ≤ f i
source
theorem le_biSup {α : Type u_1} [CompleteLattice α] {ι : Type u_8} {s : Set ι} (f : ι → α) {i : ι} (hi : i ∈ s) :
f i ≤ ⨆ i ∈ s, f i
source
theorem biInf_le_biSup {α : Type u_1} [CompleteLattice α] {ι : Type u_8} {s : Set ι} (hs : s.Nonempty) {f : ι → α} :
⨅ i ∈ s, f i ≤ ⨆ i ∈ s, f i
source
theorem iSup_sup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [Nonempty ι] {f : ι → α} {a : α} :
(⨆ (x : ι), f x) ⊔ a = ⨆ (x : ι), f x ⊔ a
source
theorem iInf_inf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [Nonempty ι] {f : ι → α} {a : α} :
(⨅ (x : ι), f x) ⊓ a = ⨅ (x : ι), f x ⊓ a
source
theorem sup_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [Nonempty ι] {f : ι → α} {a : α} :
a ⊔ ⨆ (x : ι), f x = ⨆ (x : ι), a ⊔ f x
source
theorem inf_iInf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [Nonempty ι] {f : ι → α} {a : α} :
a ⊓ ⨅ (x : ι), f x = ⨅ (x : ι), a ⊓ f x
source
theorem biSup_sup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α} (h : ∃ (i : ι), p i) :
(⨆ (i : ι), ⨆ (h : p i), f i h) ⊔ a = ⨆ (i : ι), ⨆ (h : p i), f i h ⊔ a
source
theorem sup_biSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α} (h : ∃ (i : ι), p i) :
a ⊔ ⨆ (i : ι), ⨆ (h : p i), f i h = ⨆ (i : ι), ⨆ (h : p i), a ⊔ f i h
source
theorem biInf_inf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α} (h : ∃ (i : ι), p i) :
(⨅ (i : ι), ⨅ (h : p i), f i h) ⊓ a = ⨅ (i : ι), ⨅ (h : p i), f i h ⊓ a
source
theorem inf_biInf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α} (h : ∃ (i : ι), p i) :
a ⊓ ⨅ (i : ι), ⨅ (h : p i), f i h = ⨅ (i : ι), ⨅ (h : p i), a ⊓ f i h
source
theorem biSup_lt_eq_iSup {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [LT ι] [NoMaxOrder ι] {f : ι → α} :
⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j = ⨆ (i : ι), f i
source
theorem biSup_le_eq_iSup {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [Preorder ι] {f : ι → α} :
⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≤ i), f j = ⨆ (i : ι), f i
source
theorem biInf_lt_eq_iInf {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [LT ι] [NoMaxOrder ι] {f : ι → α} :
⨅ (i : ι), ⨅ (j : ι), ⨅ (_ : j < i), f j = ⨅ (i : ι), f i
source
theorem biInf_le_eq_iInf {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [Preorder ι] {f : ι → α} :
⨅ (i : ι), ⨅ (j : ι), ⨅ (_ : j ≤ i), f j = ⨅ (i : ι), f i
source
theorem biSup_gt_eq_iSup {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [LT ι] [NoMinOrder ι] {f : ι → α} :
⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j = ⨆ (i : ι), f i
source
theorem biSup_ge_eq_iSup {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [Preorder ι] {f : ι → α} :
⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≥ i), f j = ⨆ (i : ι), f i
source
theorem biInf_gt_eq_iInf {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [LT ι] [NoMinOrder ι] {f : ι → α} :
⨅ (i : ι), ⨅ (j : ι), ⨅ (_ : j > i), f j = ⨅ (i : ι), f i
source
theorem biInf_ge_eq_iInf {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [Preorder ι] {f : ι → α} :
⨅ (i : ι), ⨅ (j : ι), ⨅ (_ : j ≥ i), f j = ⨅ (i : ι), f i
source
theorem biSup_le_eq_of_monotone {α : Type u_1} {β : Type u_2} [CompleteLattice α] [Preorder β] {f : β → α} (hf : Monotone f) (b : β) :
⨆ (b' : β), ⨆ (_ : b' ≤ b), f b' = f b
source
theorem biInf_le_eq_of_antitone {α : Type u_1} {β : Type u_2} [CompleteLattice α] [Preorder β] {f : β → α} (hf : Antitone f) (b : β) :
⨅ (b' : β), ⨅ (_ : b' ≤ b), f b' = f b
source
theorem biSup_ge_eq_of_antitone {α : Type u_1} {β : Type u_2} [CompleteLattice α] [Preorder β] {f : β → α} (hf : Antitone f) (b : β) :
⨆ (b' : β), ⨆ (_ : b' ≥ b), f b' = f b
source
theorem biInf_ge_eq_of_monotone {α : Type u_1} {β : Type u_2} [CompleteLattice α] [Preorder β] {f : β → α} (hf : Monotone f) (b : β) :
⨅ (b' : β), ⨅ (_ : b' ≥ b), f b' = f b

### `iSup` and `iInf` under `Prop` #

source
theorem iSup_false {α : Type u_1} [CompleteLattice α] {s : False → α} :
iSup s = ⊥
source
theorem iInf_false {α : Type u_1} [CompleteLattice α] {s : False → α} :
iInf s = ⊤
source
theorem iSup_true {α : Type u_1} [CompleteLattice α] {s : True → α} :
iSup s = s trivial
source
theorem iInf_true {α : Type u_1} [CompleteLattice α] {s : True → α} :
iInf s = s trivial
source
@[simp]
theorem iSup_exists {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ι → Prop} {f : Exists p → α} :
⨆ (x : Exists p), f x = ⨆ (i : ι), ⨆ (h : p i), f ⋯
source
@[simp]
theorem iInf_exists {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ι → Prop} {f : Exists p → α} :
⨅ (x : Exists p), f x = ⨅ (i : ι), ⨅ (h : p i), f ⋯
source
theorem iSup_and {α : Type u_1} [CompleteLattice α] {p q : Prop} {s : p ∧ q → α} :
iSup s = ⨆ (h₁ : p), ⨆ (h₂ : q), s ⋯
source
theorem iInf_and {α : Type u_1} [CompleteLattice α] {p q : Prop} {s : p ∧ q → α} :
iInf s = ⨅ (h₁ : p), ⨅ (h₂ : q), s ⋯
source
theorem iSup_and' {α : Type u_1} [CompleteLattice α] {p q : Prop} {s : p → q → α} :
⨆ (h₁ : p), ⨆ (h₂ : q), s h₁ h₂ = ⨆ (h : p ∧ q), s ⋯ ⋯

The symmetric case of `iSup_and`, useful for rewriting into a supremum over a conjunction

source
theorem iInf_and' {α : Type u_1} [CompleteLattice α] {p q : Prop} {s : p → q → α} :
⨅ (h₁ : p), ⨅ (h₂ : q), s h₁ h₂ = ⨅ (h : p ∧ q), s ⋯ ⋯

The symmetric case of `iInf_and`, useful for rewriting into an infimum over a conjunction

source
theorem iSup_or {α : Type u_1} [CompleteLattice α] {p q : Prop} {s : p ∨ q → α} :
⨆ (x : p ∨ q), s x = (⨆ (i : p), s ⋯) ⊔ ⨆ (j : q), s ⋯
source
theorem iInf_or {α : Type u_1} [CompleteLattice α] {p q : Prop} {s : p ∨ q → α} :
⨅ (x : p ∨ q), s x = (⨅ (i : p), s ⋯) ⊓ ⨅ (j : q), s ⋯
source
theorem iSup_dite {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (p : ι → Prop) [DecidablePred p] (f : (i : ι) → p i → α) (g : (i : ι) → ¬p i → α) :
(⨆ (i : ι), if h : p i then f i h else g i h) = (⨆ (i : ι), ⨆ (h : p i), f i h) ⊔ ⨆ (i : ι), ⨆ (h : ¬p i), g i h
source
theorem iInf_dite {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (p : ι → Prop) [DecidablePred p] (f : (i : ι) → p i → α) (g : (i : ι) → ¬p i → α) :
(⨅ (i : ι), if h : p i then f i h else g i h) = (⨅ (i : ι), ⨅ (h : p i), f i h) ⊓ ⨅ (i : ι), ⨅ (h : ¬p i), g i h
source
theorem iSup_ite {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (p : ι → Prop) [DecidablePred p] (f g : ι → α) :
(⨆ (i : ι), if p i then f i else g i) = (⨆ (i : ι), ⨆ (_ : p i), f i) ⊔ ⨆ (i : ι), ⨆ (_ : ¬p i), g i
source
theorem iInf_ite {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (p : ι → Prop) [DecidablePred p] (f g : ι → α) :
(⨅ (i : ι), if p i then f i else g i) = (⨅ (i : ι), ⨅ (_ : p i), f i) ⊓ ⨅ (i : ι), ⨅ (_ : ¬p i), g i
source
theorem iSup_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {g : β → α} {f : ι → β} :
⨆ b ∈ Set.range f, g b = ⨆ (i : ι), g (f i)
source
theorem iInf_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {g : β → α} {f : ι → β} :
⨅ b ∈ Set.range f, g b = ⨅ (i : ι), g (f i)
source
theorem sSup_image {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : β → α} :
sSup (f '' s) = ⨆ a ∈ s, f a
source
theorem sInf_image {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : β → α} :
sInf (f '' s) = ⨅ a ∈ s, f a
source
theorem OrderIso.map_sSup_eq_sSup_symm_preimage {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (s : Set α) :
f (sSup s) = sSup (⇑f.symm ⁻¹' s)
source
theorem OrderIso.map_sInf_eq_sInf_symm_preimage {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (s : Set α) :
f (sInf s) = sInf (⇑f.symm ⁻¹' s)
source
theorem iSup_emptyset {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} :
⨆ x ∈ ∅, f x = ⊥
source
theorem iInf_emptyset {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} :
⨅ x ∈ ∅, f x = ⊤
source
theorem iSup_univ {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} :
⨆ x ∈ Set.univ, f x = ⨆ (x : β), f x
source
theorem iInf_univ {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} :
⨅ x ∈ Set.univ, f x = ⨅ (x : β), f x
source
theorem iSup_union {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {s t : Set β} :
⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x
source
theorem iInf_union {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {s t : Set β} :
⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ ⨅ x ∈ t, f x
source
theorem iSup_split {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) (p : β → Prop) :
⨆ (i : β), f i = (⨆ (i : β), ⨆ (_ : p i), f i) ⊔ ⨆ (i : β), ⨆ (_ : ¬p i), f i
source
theorem iInf_split {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) (p : β → Prop) :
⨅ (i : β), f i = (⨅ (i : β), ⨅ (_ : p i), f i) ⊓ ⨅ (i : β), ⨅ (_ : ¬p i), f i
source
theorem iSup_split_single {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) (i₀ : β) :
⨆ (i : β), f i = f i₀ ⊔ ⨆ (i : β), ⨆ (_ : i ≠ i₀), f i
source
theorem iInf_split_single {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) (i₀ : β) :
⨅ (i : β), f i = f i₀ ⊓ ⨅ (i : β), ⨅ (_ : i ≠ i₀), f i
source
theorem iSup_le_iSup_of_subset {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {s t : Set β} :
s ⊆ t → ⨆ x ∈ s, f x ≤ ⨆ x ∈ t, f x
source
theorem iInf_le_iInf_of_subset {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {s t : Set β} :
s ⊆ t → ⨅ x ∈ t, f x ≤ ⨅ x ∈ s, f x
source
theorem iSup_insert {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {s : Set β} {b : β} :
⨆ x ∈ insert b s, f x = f b ⊔ ⨆ x ∈ s, f x
source
theorem iInf_insert {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {s : Set β} {b : β} :
⨅ x ∈ insert b s, f x = f b ⊓ ⨅ x ∈ s, f x
source
theorem iSup_singleton {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {b : β} :
⨆ x ∈ {b}, f x = f b
source
theorem iInf_singleton {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {b : β} :
⨅ x ∈ {b}, f x = f b
source
theorem iSup_pair {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {a b : β} :
⨆ x ∈ {a, b}, f x = f a ⊔ f b
source
theorem iInf_pair {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {a b : β} :
⨅ x ∈ {a, b}, f x = f a ⊓ f b
source
theorem iSup_image {α : Type u_1} {β : Type u_2} [CompleteLattice α] {γ : Type u_8} {f : β → γ} {g : γ → α} {t : Set β} :
⨆ c ∈ f '' t, g c = ⨆ b ∈ t, g (f b)
source
theorem iInf_image {α : Type u_1} {β : Type u_2} [CompleteLattice α] {γ : Type u_8} {f : β → γ} {g : γ → α} {t : Set β} :
⨅ c ∈ f '' t, g c = ⨅ b ∈ t, g (f b)
source
theorem iSup_extend_bot {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {e : ι → β} (he : Function.Injective e) (f : ι → α) :
⨆ (j : β), Function.extend e f ⊥ j = ⨆ (i : ι), f i
source
theorem iInf_extend_top {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {e : ι → β} (he : Function.Injective e) (f : ι → α) :
⨅ (j : β), Function.extend e f ⊤ j = iInf f
source
theorem biSup_le_eq_sup {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [PartialOrder ι] (f : ι → α) (i : ι) :
⨆ (j : ι), ⨆ (_ : j ≤ i), f j = (⨆ (j : ι), ⨆ (_ : j < i), f j) ⊔ f i
source
theorem biInf_le_eq_inf {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [PartialOrder ι] (f : ι → α) (i : ι) :
⨅ (j : ι), ⨅ (_ : j ≤ i), f j = (⨅ (j : ι), ⨅ (_ : j < i), f j) ⊓ f i
source
theorem biSup_ge_eq_sup {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [PartialOrder ι] (f : ι → α) (i : ι) :
⨆ (j : ι), ⨆ (_ : j ≥ i), f j = f i ⊔ ⨆ (j : ι), ⨆ (_ : j > i), f j
source
theorem biInf_ge_eq_inf {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [PartialOrder ι] (f : ι → α) (i : ι) :
⨅ (j : ι), ⨅ (_ : j ≥ i), f j = f i ⊓ ⨅ (j : ι), ⨅ (_ : j > i), f j

### `iSup` and `iInf` under `Type` #

source
theorem iSup_of_empty' {α : Type u_8} {ι : Sort u_9} [SupSet α] [IsEmpty ι] (f : ι → α) :
iSup f = sSup ∅
source
theorem iInf_of_isEmpty {α : Type u_8} {ι : Sort u_9} [InfSet α] [IsEmpty ι] (f : ι → α) :
iInf f = sInf ∅
source
theorem iSup_of_empty {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [IsEmpty ι] (f : ι → α) :
iSup f = ⊥
source
theorem iInf_of_empty {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [IsEmpty ι] (f : ι → α) :
iInf f = ⊤
source
theorem isGLB_biInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : β → α} :
IsGLB (f '' s) (⨅ x ∈ s, f x)
source
theorem isLUB_biSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : β → α} :
IsLUB (f '' s) (⨆ x ∈ s, f x)
source
theorem iSup_sigma {α : Type u_1} {β : Type u_2} [CompleteLattice α] {p : β → Type u_8} {f : Sigma p → α} :
⨆ (x : Sigma p), f x = ⨆ (i : β), ⨆ (j : p i), f ⟨i, j⟩
source
theorem iInf_sigma {α : Type u_1} {β : Type u_2} [CompleteLattice α] {p : β → Type u_8} {f : Sigma p → α} :
⨅ (x : Sigma p), f x = ⨅ (i : β), ⨅ (j : p i), f ⟨i, j⟩
source
theorem iSup_sigma' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {κ : β → Type u_8} (f : (i : β) → κ i → α) :
⨆ (i : β), ⨆ (j : κ i), f i j = ⨆ (x : (i : β) × κ i), f x.fst x.snd
source
theorem iInf_sigma' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {κ : β → Type u_8} (f : (i : β) → κ i → α) :
⨅ (i : β), ⨅ (j : κ i), f i j = ⨅ (x : (i : β) × κ i), f x.fst x.snd
source
theorem iSup_psigma {α : Type u_1} [CompleteLattice α] {ι : Sort u_8} {κ : ι → Sort u_9} (f : (i : ι) ×' κ i → α) :
⨆ (ij : (i : ι) ×' κ i), f ij = ⨆ (i : ι), ⨆ (j : κ i), f ⟨i, j⟩
source
theorem iInf_psigma {α : Type u_1} [CompleteLattice α] {ι : Sort u_8} {κ : ι → Sort u_9} (f : (i : ι) ×' κ i → α) :
⨅ (ij : (i : ι) ×' κ i), f ij = ⨅ (i : ι), ⨅ (j : κ i), f ⟨i, j⟩
source
theorem iSup_psigma' {α : Type u_1} [CompleteLattice α] {ι : Sort u_8} {κ : ι → Sort u_9} (f : (i : ι) → κ i → α) :
⨆ (i : ι), ⨆ (j : κ i), f i j = ⨆ (ij : (i : ι) ×' κ i), f ij.fst ij.snd
source
theorem iInf_psigma' {α : Type u_1} [CompleteLattice α] {ι : Sort u_8} {κ : ι → Sort u_9} (f : (i : ι) → κ i → α) :
⨅ (i : ι), ⨅ (j : κ i), f i j = ⨅ (ij : (i : ι) ×' κ i), f ij.fst ij.snd
source
theorem iSup_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β × γ → α} :
⨆ (x : β × γ), f x = ⨆ (i : β), ⨆ (j : γ), f (i, j)
source
theorem iInf_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β × γ → α} :
⨅ (x : β × γ), f x = ⨅ (i : β), ⨅ (j : γ), f (i, j)
source
theorem iSup_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] (f : β → γ → α) :
⨆ (i : β), ⨆ (j : γ), f i j = ⨆ (x : β × γ), f x.1 x.2
source
theorem iInf_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] (f : β → γ → α) :
⨅ (i : β), ⨅ (j : γ), f i j = ⨅ (x : β × γ), f x.1 x.2
source
theorem biSup_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β × γ → α} {s : Set β} {t : Set γ} :
⨆ x ∈ s ×ˢ t, f x = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)
source
theorem biSup_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ} :
⨆ x ∈ s ×ˢ t, f x.1 x.2 = ⨆ a ∈ s, ⨆ b ∈ t, f a b
source
theorem biInf_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β × γ → α} {s : Set β} {t : Set γ} :
⨅ x ∈ s ×ˢ t, f x = ⨅ a ∈ s, ⨅ b ∈ t, f (a, b)
source
theorem biInf_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ} :
⨅ x ∈ s ×ˢ t, f x.1 x.2 = ⨅ a ∈ s, ⨅ b ∈ t, f a b
source
theorem iSup_image2 {α : Type u_1} {β : Type u_2} [CompleteLattice α] {γ : Type u_8} {δ : Type u_9} (f : β → γ → δ) (s : Set β) (t : Set γ) (g : δ → α) :
⨆ d ∈ Set.image2 f s t, g d = ⨆ b ∈ s, ⨆ c ∈ t, g (f b c)
source
theorem iInf_image2 {α : Type u_1} {β : Type u_2} [CompleteLattice α] {γ : Type u_8} {δ : Type u_9} (f : β → γ → δ) (s : Set β) (t : Set γ) (g : δ → α) :
⨅ d ∈ Set.image2 f s t, g d = ⨅ b ∈ s, ⨅ c ∈ t, g (f b c)
source
theorem iSup_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β ⊕ γ → α} :
⨆ (x : β ⊕ γ), f x = (⨆ (i : β), f (Sum.inl i)) ⊔ ⨆ (j : γ), f (Sum.inr j)
source
theorem iInf_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β ⊕ γ → α} :
⨅ (x : β ⊕ γ), f x = (⨅ (i : β), f (Sum.inl i)) ⊓ ⨅ (j : γ), f (Sum.inr j)
source
theorem iSup_option {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : Option β → α) :
⨆ (o : Option β), f o = f none ⊔ ⨆ (b : β), f (some b)
source
theorem iInf_option {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : Option β → α) :
⨅ (o : Option β), f o = f none ⊓ ⨅ (b : β), f (some b)
source
theorem iSup_option_elim {α : Type u_1} {β : Type u_2} [CompleteLattice α] (a : α) (f : β → α) :
⨆ (o : Option β), o.elim a f = a ⊔ ⨆ (b : β), f b

A version of `iSup_option` useful for rewriting right-to-left.

source
theorem iInf_option_elim {α : Type u_1} {β : Type u_2} [CompleteLattice α] (a : α) (f : β → α) :
⨅ (o : Option β), o.elim a f = a ⊓ ⨅ (b : β), f b

A version of `iInf_option` useful for rewriting right-to-left.

source
@[simp]
theorem iSup_ne_bot_subtype {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ι → α) :
⨆ (i : { i : ι // f i ≠ ⊥ }), f ↑i = ⨆ (i : ι), f i

When taking the supremum of `f : ι → α`, the elements of `ι` on which `f` gives `⊥` can be dropped, without changing the result.

source
theorem iInf_ne_top_subtype {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ι → α) :
⨅ (i : { i : ι // f i ≠ ⊤ }), f ↑i = ⨅ (i : ι), f i

When taking the infimum of `f : ι → α`, the elements of `ι` on which `f` gives `⊤` can be dropped, without changing the result.

source
theorem sSup_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ} :
sSup (Set.image2 f s t) = ⨆ a ∈ s, ⨆ b ∈ t, f a b
source
theorem sInf_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ} :
sInf (Set.image2 f s t) = ⨅ a ∈ s, ⨅ b ∈ t, f a b
source
theorem iSup_eq_top {α : Type u_1} {ι : Sort u_4} [CompleteLinearOrder α] (f : ι → α) :
iSup f = ⊤ ↔ ∀ b < ⊤, ∃ (i : ι), b < f i
source
theorem iInf_eq_bot {α : Type u_1} {ι : Sort u_4} [CompleteLinearOrder α] (f : ι → α) :
iInf f = ⊥ ↔ ∀ b > ⊥, ∃ (i : ι), f i < b
source
theorem iSup₂_eq_top {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLinearOrder α] (f : (i : ι) → κ i → α) :
⨆ (i : ι), ⨆ (j : κ i), f i j = ⊤ ↔ ∀ b < ⊤, ∃ (i : ι) (j : κ i), b < f i j
source
theorem iInf₂_eq_bot {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [CompleteLinearOrder α] (f : (i : ι) → κ i → α) :
⨅ (i : ι), ⨅ (j : κ i), f i j = ⊥ ↔ ∀ b > ⊥, ∃ (i : ι) (j : κ i), f i j < b

### Instances #

source
instance Prop.instCompleteLattice :
CompleteLattice Prop
Equations

- One or more equations did not get rendered due to their size.

source
noncomputable instance Prop.instCompleteLinearOrder :
CompleteLinearOrder Prop
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem sSup_Prop_eq {s : Set Prop} :
sSup s = ∃ p ∈ s, p
source
@[simp]
theorem sInf_Prop_eq {s : Set Prop} :
sInf s = ∀ p ∈ s, p
source
@[simp]
theorem iSup_Prop_eq {ι : Sort u_4} {p : ι → Prop} :
⨆ (i : ι), p i = ∃ (i : ι), p i
source
@[simp]
theorem iInf_Prop_eq {ι : Sort u_4} {p : ι → Prop} :
⨅ (i : ι), p i = ∀ (i : ι), p i
source
instance Pi.supSet {α : Type u_8} {β : α → Type u_9} [(i : α) → SupSet (β i)] :
SupSet ((i : α) → β i)
Equations

- Pi.supSet = { sSup := fun (s : Set ((i : α) → β i)) (i : α) => ⨆ (f : ↑s), ↑f i }

source
instance Pi.infSet {α : Type u_8} {β : α → Type u_9} [(i : α) → InfSet (β i)] :
InfSet ((i : α) → β i)
Equations

- Pi.infSet = { sInf := fun (s : Set ((i : α) → β i)) (i : α) => ⨅ (f : ↑s), ↑f i }

source
instance Pi.instCompleteLattice {α : Type u_8} {β : α → Type u_9} [(i : α) → CompleteLattice (β i)] :
CompleteLattice ((i : α) → β i)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem sSup_apply {α : Type u_8} {β : α → Type u_9} [(i : α) → SupSet (β i)] {s : Set ((a : α) → β a)} {a : α} :
sSup s a = ⨆ (f : ↑s), ↑f a
source
@[simp]
theorem sInf_apply {α : Type u_8} {β : α → Type u_9} [(i : α) → InfSet (β i)] {s : Set ((a : α) → β a)} {a : α} :
sInf s a = ⨅ (f : ↑s), ↑f a
source
@[simp]
theorem iSup_apply {α : Type u_8} {β : α → Type u_9} {ι : Sort u_10} [(i : α) → SupSet (β i)] {f : ι → (a : α) → β a} {a : α} :
(⨆ (i : ι), f i) a = ⨆ (i : ι), f i a
source
@[simp]
theorem iInf_apply {α : Type u_8} {β : α → Type u_9} {ι : Sort u_10} [(i : α) → InfSet (β i)] {f : ι → (a : α) → β a} {a : α} :
(⨅ (i : ι), f i) a = ⨅ (i : ι), f i a
source
theorem unary_relation_sSup_iff {α : Type u_8} (s : Set (α → Prop)) {a : α} :
sSup s a ↔ ∃ r ∈ s, r a
source
theorem unary_relation_sInf_iff {α : Type u_8} (s : Set (α → Prop)) {a : α} :
sInf s a ↔ ∀ r ∈ s, r a
source
theorem binary_relation_sSup_iff {α : Type u_8} {β : Type u_9} (s : Set (α → β → Prop)) {a : α} {b : β} :
sSup s a b ↔ ∃ r ∈ s, r a b
source
theorem binary_relation_sInf_iff {α : Type u_8} {β : Type u_9} (s : Set (α → β → Prop)) {a : α} {b : β} :
sInf s a b ↔ ∀ r ∈ s, r a b
source
theorem Monotone.sSup {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (α → β)} (hs : ∀ f ∈ s, Monotone f) :
Monotone (sSup s)
source
theorem Monotone.sInf {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (α → β)} (hs : ∀ f ∈ s, Monotone f) :
Monotone (sInf s)
source
theorem Antitone.sSup {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (α → β)} (hs : ∀ f ∈ s, Antitone f) :
Antitone (sSup s)
source
theorem Antitone.sInf {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (α → β)} (hs : ∀ f ∈ s, Antitone f) :
Antitone (sInf s)
source
theorem Monotone.iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Preorder α] [CompleteLattice β] {f : ι → α → β} (hf : ∀ (i : ι), Monotone (f i)) :
Monotone (⨆ (i : ι), f i)
source
theorem Monotone.iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Preorder α] [CompleteLattice β] {f : ι → α → β} (hf : ∀ (i : ι), Monotone (f i)) :
Monotone (⨅ (i : ι), f i)
source
theorem Antitone.iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Preorder α] [CompleteLattice β] {f : ι → α → β} (hf : ∀ (i : ι), Antitone (f i)) :
Antitone (⨆ (i : ι), f i)
source
theorem Antitone.iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Preorder α] [CompleteLattice β] {f : ι → α → β} (hf : ∀ (i : ι), Antitone (f i)) :
Antitone (⨅ (i : ι), f i)
source
instance Prod.supSet (α : Type u_1) (β : Type u_2) [SupSet α] [SupSet β] :
SupSet (α × β)
Equations

- Prod.supSet α β = { sSup := fun (s : Set (α × β)) => (sSup (Prod.fst '' s), sSup (Prod.snd '' s)) }

source
instance Prod.infSet (α : Type u_1) (β : Type u_2) [InfSet α] [InfSet β] :
InfSet (α × β)
Equations

- Prod.infSet α β = { sInf := fun (s : Set (α × β)) => (sInf (Prod.fst '' s), sInf (Prod.snd '' s)) }

source
theorem Prod.fst_sInf {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] (s : Set (α × β)) :
(sInf s).1 = sInf (fst '' s)
source
theorem Prod.snd_sInf {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] (s : Set (α × β)) :
(sInf s).2 = sInf (snd '' s)
source
theorem Prod.swap_sInf {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] (s : Set (α × β)) :
(sInf s).swap = sInf (swap '' s)
source
theorem Prod.fst_sSup {α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] (s : Set (α × β)) :
(sSup s).1 = sSup (fst '' s)
source
theorem Prod.snd_sSup {α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] (s : Set (α × β)) :
(sSup s).2 = sSup (snd '' s)
source
theorem Prod.swap_sSup {α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] (s : Set (α × β)) :
(sSup s).swap = sSup (swap '' s)
source
theorem Prod.fst_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [InfSet α] [InfSet β] (f : ι → α × β) :
(iInf f).1 = ⨅ (i : ι), (f i).1
source
theorem Prod.snd_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [InfSet α] [InfSet β] (f : ι → α × β) :
(iInf f).2 = ⨅ (i : ι), (f i).2
source
theorem Prod.swap_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [InfSet α] [InfSet β] (f : ι → α × β) :
(iInf f).swap = ⨅ (i : ι), (f i).swap
source
theorem Prod.iInf_mk {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [InfSet α] [InfSet β] (f : ι → α) (g : ι → β) :
⨅ (i : ι), (f i, g i) = (⨅ (i : ι), f i, ⨅ (i : ι), g i)
source
theorem Prod.fst_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [SupSet α] [SupSet β] (f : ι → α × β) :
(iSup f).1 = ⨆ (i : ι), (f i).1
source
theorem Prod.snd_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [SupSet α] [SupSet β] (f : ι → α × β) :
(iSup f).2 = ⨆ (i : ι), (f i).2
source
theorem Prod.swap_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [SupSet α] [SupSet β] (f : ι → α × β) :
(iSup f).swap = ⨆ (i : ι), (f i).swap
source
theorem Prod.iSup_mk {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [SupSet α] [SupSet β] (f : ι → α) (g : ι → β) :
⨆ (i : ι), (f i, g i) = (⨆ (i : ι), f i, ⨆ (i : ι), g i)
source
instance Prod.instCompleteLattice {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] :
CompleteLattice (α × β)
Equations

- One or more equations did not get rendered due to their size.

source
theorem sInf_prod {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) :
sInf (s ×ˢ t) = (sInf s, sInf t)
source
theorem sSup_prod {α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) :
sSup (s ×ˢ t) = (sSup s, sSup t)
source
@[reducible, inline]
abbrev Function.Injective.completeLattice {α : Type u_1} {β : Type u_2} [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [CompleteLattice β] (f : α → β) (hf : Injective f) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) :
CompleteLattice α

Pullback a `CompleteLattice` along an injection.

Equations

- One or more equations did not get rendered due to their size.

Instances For