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_5}
{s : Set ι}
(hs : s.Nonempty)
{α : Type u_6}
[CompleteLattice α]
(f : ι → α)
:
theorem
WithBot.coe_biInf
{ι : Type u_5}
{s : Set ι}
{α : Type u_6}
[CompleteLattice α]
(f : ι → α)
:
theorem
isLUB_ciSup
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{f : ι → α}
(H : BddAbove (Set.range f))
:
theorem
isLUB_ciSup_set
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : β → α}
{s : Set β}
(H : BddAbove (f '' s))
(Hne : s.Nonempty)
:
theorem
isGLB_ciInf
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{f : ι → α}
(H : BddBelow (Set.range f))
:
theorem
isGLB_ciInf_set
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : β → α}
{s : Set β}
(H : BddBelow (f '' s))
(Hne : s.Nonempty)
:
theorem
IsLUB.ciSup_eq
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{a : α}
[Nonempty ι]
{f : ι → α}
(H : IsLUB (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_eq
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{a : α}
[Nonempty ι]
{f : ι → α}
(H : IsGLB (Set.range f) a)
:
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
ciSup_mono
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{f g : ι → α}
(B : BddAbove (Set.range g))
(H : ∀ (x : ι), f x ≤ g x)
:
The indexed suprema of two functions are comparable if the functions are pointwise comparable
theorem
le_ciSup_set
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : β → α}
{s : Set β}
(H : BddAbove (f '' s))
{c : β}
(hc : c ∈ s)
:
theorem
ciInf_mono
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{f g : ι → α}
(B : BddBelow (Set.range f))
(H : ∀ (x : ι), f x ≤ g x)
:
The indexed infimum of two functions are comparable if the functions are pointwise comparable
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
ciInf_set_le
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : β → α}
{s : Set β}
(H : BddBelow (f '' s))
{c : β}
(hc : c ∈ s)
:
theorem
ciInf_le_ciSup
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{f : ι → α}
(hf : BddBelow (Set.range f))
(hf' : BddAbove (Set.range f))
:
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.
theorem
Set.Iic_ciInf
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{f : ι → α}
(hf : BddBelow (range f))
:
theorem
Set.Ici_ciSup
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{f : ι → α}
(hf : BddAbove (range f))
:
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 α]
{a : α}
[Nonempty ι]
{f : ι → α}
(h : iInf f < a)
:
∃ (i : ι), f i < a
Indexed version of exists_lt_of_csInf_lt.
When iInf f < a, there is an element i such that f i < a.
theorem
ciInf_mem
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
[WellFoundedLT α]
[Nonempty ι]
(f : ι → α)
:
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.
@[simp]
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
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
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.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.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.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_csInf
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{s : Set β}
(hne : s.Nonempty)
(hbdd : BddBelow s)
:
theorem
GaloisConnection.u_csInf'
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{s : Set β}
(hne : s.Nonempty)
(hbdd : BddBelow s)
:
theorem
GaloisConnection.u_ciInf
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
[Nonempty ι]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{f : ι → β}
(hf : BddBelow (Set.range f))
:
theorem
GaloisConnection.u_ciInf_set
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{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_csSup'
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
(e : α ≃o β)
{s : Set α}
(hne : s.Nonempty)
(hbdd : BddAbove 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_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_csInf
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
(e : α ≃o β)
{s : Set α}
(hne : s.Nonempty)
(hbdd : BddBelow 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_ciInf
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[ConditionallyCompleteLattice β]
[Nonempty ι]
(e : α ≃o β)
{f : ι → α}
(hf : BddBelow (Set.range f))
:
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_eq_top
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
{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 : ι → α}
: