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
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)
:
⨆ (i : ι), f i = 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)
:
⨆ (i : ↑s), f ↑i = a
theorem
IsGLB.ciInf_eq
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{a : α}
[Nonempty ι]
{f : ι → α}
(H : IsGLB (Set.range f) a)
:
⨅ (i : ι), f i = 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)
:
⨅ (i : ↑s), f ↑i = a
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
le_ciSup_set
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : β → α}
{s : Set β}
(H : BddAbove (f '' s))
{c : β}
(hc : c ∈ s)
:
f c ≤ ⨆ (i : ↑s), f ↑i
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)
:
⨅ (i : ↑s), f ↑i ≤ f c
@[simp]
theorem
ciSup_const
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[hι : Nonempty ι]
{a : α}
:
⨆ (x : ι), a = a
@[simp]
theorem
ciInf_const
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{a : α}
:
⨅ (x : ι), a = a
@[simp]
theorem
ciSup_unique
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Unique ι]
{s : ι → α}
:
⨆ (i : ι), s i = s default
@[simp]
theorem
ciInf_unique
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Unique ι]
{s : ι → α}
:
⨅ (i : ι), s i = s default
theorem
ciSup_subsingleton
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Subsingleton ι]
(i : ι)
(s : ι → α)
:
⨆ (i : ι), s i = s i
theorem
ciInf_subsingleton
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Subsingleton ι]
(i : ι)
(s : ι → α)
:
⨅ (i : ι), s i = s i
theorem
ciSup_eq_ite
{α : Type u_1}
[ConditionallyCompleteLattice α]
{p : Prop}
[Decidable p]
{f : p → α}
:
theorem
ciInf_eq_ite
{α : Type u_1}
[ConditionallyCompleteLattice α]
{p : Prop}
[Decidable p]
{f : p → α}
:
theorem
cbiSup_eq_of_forall
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{p : ι → Prop}
{f : Subtype p → α}
(hp : ∀ (i : ι), p i)
:
theorem
cbiInf_eq_of_forall
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{p : ι → Prop}
{f : Subtype p → α}
(hp : ∀ (i : ι), p i)
:
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)
:
⨆ (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 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)
:
⨅ (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 iInf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in complete lattices.
theorem
Monotone.ciSup_mem_iInter_Icc_of_antitone
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[SemilatticeSup β]
{f g : β → α}
(hf : Monotone f)
(hg : Antitone g)
(h : f ≤ g)
:
Nested intervals lemma: if f is a monotone sequence, g is an antitone sequence, and
f n ≤ g n for all n, then ⨆ n, f n belongs to all the intervals [f n, g n].
theorem
ciSup_mem_iInter_Icc_of_antitone_Icc
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
[SemilatticeSup β]
{f g : β → α}
(h : Antitone fun (n : β) => Set.Icc (f n) (g n))
(h' : ∀ (n : β), f n ≤ g n)
:
Nested intervals lemma: if [f n, g n] is an antitone sequence of nonempty
closed intervals, then ⨆ n, f n belongs to all the intervals [f n, g n].
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))
:
l (⨆ (i : ι), f i) = ⨆ (i : ι), l (f i)
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)
:
l (⨆ (i : ↑s), f ↑i) = ⨆ (i : ↑s), l (f ↑i)
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))
:
u (⨅ (i : ι), f i) = ⨅ (i : ι), u (f i)
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)
:
u (⨅ (i : ↑s), f ↑i) = ⨅ (i : ↑s), u (f ↑i)
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))
:
e (⨆ (i : ι), f i) = ⨆ (i : ι), e (f i)
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)
:
e (⨆ (i : ↑s), f ↑i) = ⨆ (i : ↑s), e (f ↑i)
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))
:
e (⨅ (i : ι), f i) = ⨅ (i : ι), e (f i)
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)
:
e (⨅ (i : ↑s), f ↑i) = ⨅ (i : ↑s), e (f ↑i)
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 : ι → α}
: