Indexed sup / inf in conditionally complete lattices #
This file proves lemmas about iSup and iInf for functions valued in a conditionally complete,
rather than complete, lattice. We add a prefix c to distinguish them from the versions for
complete lattices, giving names ciSup_xxx or ciInf_xxx.
theorem
WithBot.coe_biSup
{ι : Type u_6}
{s : Set ι}
(hs : s.Nonempty)
{α : Type u_7}
[CompleteLattice α]
(f : ι → α)
:
theorem
WithTop.coe_biInf
{ι : Type u_6}
{s : Set ι}
(hs : s.Nonempty)
{α : Type u_7}
[CompleteLattice α]
(f : ι → α)
:
theorem
WithBot.coe_biInf
{ι : Type u_6}
{s : Set ι}
{α : Type u_7}
[CompleteLattice α]
(f : ι → α)
:
theorem
WithTop.coe_biSup
{ι : Type u_6}
{s : Set ι}
{α : Type u_7}
[CompleteLattice α]
(f : ι → α)
:
theorem
isLUB_ciSup
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{f : ι → α}
(H : BddAbove (Set.range f))
:
theorem
isGLB_ciInf
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{f : ι → α}
(H : BddBelow (Set.range f))
:
theorem
IsLUB.ciSup_eq
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{a : α}
[Nonempty ι]
{f : ι → α}
(H : IsLUB (Set.range f) a)
:
theorem
IsGLB.ciInf_eq
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{a : α}
[Nonempty ι]
{f : ι → α}
(H : IsGLB (Set.range f) a)
:
theorem
IsLUB.ciSup_set_eq
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{a : α}
{s : Set β}
{f : β → α}
(H : IsLUB (f '' s) a)
(Hne : s.Nonempty)
:
theorem
IsGLB.ciInf_set_eq
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{a : α}
{s : Set β}
{f : β → α}
(H : IsGLB (f '' s) a)
(Hne : s.Nonempty)
:
theorem
le_ciSup_of_le
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{a : α}
{f : ι → α}
(H : BddAbove (Set.range f))
(c : ι)
(h : a ≤ f c)
:
theorem
ciInf_le_of_le
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{a : α}
{f : ι → α}
(H : BddBelow (Set.range f))
(c : ι)
(h : f c ≤ a)
:
theorem
BddAbove.range_iSup_of_iUnion_range
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{κ : ι → Sort u_6}
{f : (i : ι) → κ i → α}
(H : BddAbove (⋃ (i : ι), Set.range (f i)))
:
If the set of all f i j is bounded above, then so is the set of the supremums of every row
theorem
BddBelow.range_iInf_of_iUnion_range
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{κ : ι → Sort u_6}
{f : (i : ι) → κ i → α}
(H : BddBelow (⋃ (i : ι), Set.range (f i)))
:
If the set of all f i j is bounded below, then so is the set of the infimums of
every row
theorem
ciSup_sup_eq
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{f g : ι → α}
(Hf : BddAbove (Set.range f))
(Hg : BddAbove (Set.range g))
:
theorem
ciInf_inf_eq
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{f g : ι → α}
(Hf : BddBelow (Set.range f))
(Hg : BddBelow (Set.range g))
:
theorem
le_ciSup_set
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : β → α}
{s : Set β}
(H : BddAbove (f '' s))
{c : β}
(hc : c ∈ s)
:
theorem
ciInf_set_le
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : β → α}
{s : Set β}
(H : BddBelow (f '' s))
{c : β}
(hc : c ∈ s)
:
theorem
ciSup_eq_of_forall_le_of_forall_lt_exists_gt
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{b : α}
[Nonempty ι]
{f : ι → α}
(h₁ : ∀ (i : ι), f i ≤ b)
(h₂ : ∀ w < b, ∃ (i : ι), w < f i)
:
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 iSup_eq_of_forall_le_of_forall_lt_exists_gt for a version in complete lattices.
theorem
ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{b : α}
[Nonempty ι]
{f : ι → α}
(h₁ : ∀ (i : ι), b ≤ f i)
(h₂ : ∀ (w : α), b < w → ∃ (i : ι), f i < w)
:
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 iInf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in
complete lattices.
@[deprecated cbiSup_eq_ciSup_subtype (since := "2026-04-04")]
theorem
ciSup_subtype'
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{p : ι → Prop}
{f : (i : ι) → p i → α}
(hf : BddAbove (Set.range fun (i : Subtype p) => f ↑i ⋯))
(hf' : sSup ∅ ≤ ⨆ (i : Subtype p), f ↑i ⋯)
:
Alias of cbiSup_eq_ciSup_subtype.
@[deprecated cbiInf_eq_ciInf_subtype (since := "2026-04-04")]
theorem
ciInf_subtype'
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{p : ι → Prop}
{f : (i : ι) → p i → α}
(hf : BddBelow (Set.range fun (i : Subtype p) => f ↑i ⋯))
(hf' : ⨅ (i : Subtype p), f ↑i ⋯ ≤ sInf ∅)
:
Alias of cbiInf_eq_ciInf_subtype.
@[deprecated ciSup_subtype_fun (since := "2026-04-04")]
theorem
ciSup_subtype''
{α : Type u_1}
[ConditionallyCompleteLattice α]
{ι : Type u_6}
{s : Set ι}
{f : ι → α}
(hf : BddAbove (Set.range fun (i : ↑s) => f ↑i))
(hf' : sSup ∅ ≤ ⨆ (i : ↑s), f ↑i)
:
Alias of ciSup_subtype_fun.
@[deprecated ciInf_subtype_fun (since := "2026-04-04")]
theorem
ciInf_subtype''
{α : Type u_1}
[ConditionallyCompleteLattice α]
{ι : Type u_6}
{s : Set ι}
{f : ι → α}
(hf : BddBelow (Set.range fun (i : ↑s) => f ↑i))
(hf' : ⨅ (i : ↑s), f ↑i ≤ sInf ∅)
:
Alias of ciInf_subtype_fun.
theorem
le_ciSup_ciSup_eq_left
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{b : β}
{f : (x : β) → x = b → α}
:
theorem
ciInf_ciInf_eq_left_le
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{b : β}
{f : (x : β) → x = b → α}
:
theorem
le_ciSup_ciSup_eq_right
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{b : β}
{f : (x : β) → b = x → α}
:
theorem
ciInf_ciInf_eq_right_le
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{b : β}
{f : (x : β) → b = x → α}
:
theorem
ciSup_exists_le
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{p : ι → Prop}
{f : Exists p → α}
:
Note that equality need not hold: consider ι := Bool, p := (·), α := ℤ, f := fun _ ↦ -1,
then the LHS is -1 but the RHS is -1 ⊔ sSup ∅ = -1 ⊔ 0 = 0.
theorem
le_ciInf_exists
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{p : ι → Prop}
{f : Exists p → α}
:
theorem
ciSup_sup_le
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
{f g : ι → α}
:
theorem
ciInf_inf_le
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
{f g : ι → α}
:
theorem
exists_lt_of_lt_ciSup
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
{b : α}
[Nonempty ι]
{f : ι → α}
(h : b < iSup f)
:
∃ (i : ι), b < f i
Indexed version of exists_lt_of_lt_csSup.
When b < iSup f, there is an element i such that b < f i.
theorem
exists_lt_of_ciInf_lt
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
{b : α}
[Nonempty ι]
{f : ι → α}
(h : iInf f < b)
:
∃ (i : ι), f i < b
Indexed version of exists_lt_of_csInf_lt.
When iInf f < a, there is an element i such that f i < a.
theorem
exists_lt_of_lt_ciSup₂
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_5}
[ConditionallyCompleteLinearOrder α]
{a : α}
[Nonempty ι]
[∀ (i : ι), Nonempty (κ i)]
{f : (i : ι) → κ i → α}
(h : a < ⨆ (i : ι), ⨆ (j : κ i), f i j)
:
∃ (i : ι) (j : κ i), a < f i j
theorem
exists_lt_of_ciInf₂_lt
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_5}
[ConditionallyCompleteLinearOrder α]
{a : α}
[Nonempty ι]
[∀ (i : ι), Nonempty (κ i)]
{f : (i : ι) → κ i → α}
(h : ⨅ (i : ι), ⨅ (j : κ i), f i j < a)
:
∃ (i : ι) (j : κ i), f i j < a
@[deprecated ciSup_eq_top_of_top_mem (since := "2026-04-05")]
theorem
ciInf_eq_top_of_top_mem
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
[OrderTop α]
{f : ι → α}
(hs : ⊤ ∈ Set.range f)
:
Alias of ciSup_eq_top_of_top_mem.
theorem
ciInf_mem
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
[WellFoundedLT α]
[Nonempty ι]
(f : ι → α)
:
theorem
ciInf_eq_iff
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
[WellFoundedLT α]
[Nonempty ι]
(f : ι → α)
(n : α)
:
Lemmas about a conditionally complete linear order with bottom element #
In this case we have Sup ∅ = ⊥, so we can drop some Nonempty/Set.Nonempty assumptions.
theorem
ciSup_of_empty
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
[IsEmpty ι]
(f : ι → α)
:
theorem
le_ciInf_iff'
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
[Nonempty ι]
{f : ι → α}
{a : α}
:
theorem
ciInf_le_of_le'
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
{f : ι → α}
{a : α}
(c : ι)
:
theorem
ciSup_le_iff'
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
{f : ι → α}
(h : BddAbove (Set.range f))
{a : α}
:
In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from ciSup_le_iff.
theorem
ciSup₂_le'
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_5}
[ConditionallyCompleteLinearOrderBot α]
{a : α}
{f : (i : ι) → κ i → α}
(h : ∀ (i : ι) (j : κ i), f i j ≤ a)
:
theorem
lt_ciSup_iff'
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
{a : α}
{f : ι → α}
(h : BddAbove (Set.range f))
:
In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from lt_ciSup_iff.
theorem
exists_lt_of_lt_ciSup'
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
{f : ι → α}
{a : α}
(h : a < ⨆ (i : ι), f i)
:
∃ (i : ι), a < f i
theorem
exists_lt_of_lt_ciSup₂'
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_5}
[ConditionallyCompleteLinearOrderBot α]
{a : α}
{f : (i : ι) → κ i → α}
(h : a < ⨆ (i : ι), ⨆ (j : κ i), f i j)
:
∃ (i : ι) (j : κ i), a < f i j
theorem
ciSup_mono_of_forall_exists'
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
{ι' : Sort u_6}
{f : ι → α}
{g : ι' → α}
(hg : BddAbove (Set.range g))
(h : ∀ (i : ι), ∃ (i' : ι'), f i ≤ g i')
:
@[deprecated ciSup_mono_of_forall_exists' (since := "2026-05-03")]
theorem
ciSup_mono'
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
{ι' : Sort u_6}
{f : ι → α}
{g : ι' → α}
(hg : BddAbove (Set.range g))
(h : ∀ (i : ι), ∃ (i' : ι'), f i ≤ g i')
:
Alias of ciSup_mono_of_forall_exists'.
theorem
ciSup_exists
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
{p : ι → Prop}
{f : Exists p → α}
:
@[simp]
theorem
ciSup_ciSup_eq_left
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{b : β}
{f : (x : β) → x = b → α}
:
@[simp]
theorem
ciSup_ciSup_eq_right
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
{b : β}
{f : (x : β) → b = x → α}
:
theorem
GaloisConnection.l_csSup
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{s : Set α}
(hne : s.Nonempty)
(hbdd : BddAbove s)
:
theorem
GaloisConnection.u_csInf
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection u l)
{s : Set α}
(hne : s.Nonempty)
(hbdd : BddBelow s)
:
theorem
GaloisConnection.l_csSup'
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{s : Set α}
(hne : s.Nonempty)
(hbdd : BddAbove s)
:
theorem
GaloisConnection.u_csInf'
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection u l)
{s : Set α}
(hne : s.Nonempty)
(hbdd : BddBelow s)
:
theorem
GaloisConnection.l_ciSup
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
[Nonempty ι]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{f : ι → α}
(hf : BddAbove (Set.range f))
:
theorem
GaloisConnection.u_ciInf
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
[Nonempty ι]
{l : α → β}
{u : β → α}
(gc : GaloisConnection u l)
{f : ι → α}
(hf : BddBelow (Set.range f))
:
theorem
GaloisConnection.l_ciSup_set
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{s : Set γ}
{f : γ → α}
(hf : BddAbove (f '' s))
(hne : s.Nonempty)
:
theorem
GaloisConnection.u_ciInf_set
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection u l)
{s : Set γ}
{f : γ → α}
(hf : BddBelow (f '' s))
(hne : s.Nonempty)
:
theorem
OrderIso.map_csSup
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
(e : α ≃o β)
{s : Set α}
(hne : s.Nonempty)
(hbdd : BddAbove s)
:
theorem
OrderIso.map_csInf
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
(e : α ≃o β)
{s : Set α}
(hne : s.Nonempty)
(hbdd : BddBelow s)
:
theorem
OrderIso.map_csSup'
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
(e : α ≃o β)
{s : Set α}
(hne : s.Nonempty)
(hbdd : BddAbove s)
:
theorem
OrderIso.map_csInf'
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
(e : α ≃o β)
{s : Set α}
(hne : s.Nonempty)
(hbdd : BddBelow s)
:
theorem
OrderIso.map_ciSup
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
[Nonempty ι]
(e : α ≃o β)
{f : ι → α}
(hf : BddAbove (Set.range f))
:
theorem
OrderIso.map_ciInf
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
[Nonempty ι]
(e : α ≃o β)
{f : ι → α}
(hf : BddBelow (Set.range f))
:
theorem
OrderIso.map_ciSup_set
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
(e : α ≃o β)
{s : Set γ}
{f : γ → α}
(hf : BddAbove (f '' s))
(hne : s.Nonempty)
:
theorem
OrderIso.map_ciInf_set
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
(e : α ≃o β)
{s : Set γ}
{f : γ → α}
(hf : BddBelow (f '' s))
(hne : s.Nonempty)
:
@[simp]
theorem
OrderIso.map_ciSup'
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
[ConditionallyCompleteLinearOrderBot β]
(e : α ≃o β)
(f : ι → α)
:
theorem
WithTop.iSup_coe_lt_top
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
{f : ι → α}
:
theorem
WithTop.iInf_coe_eq_top
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
{f : ι → α}
:
theorem
WithTop.iInf_coe_lt_top
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
{f : ι → α}
: