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.
@[simp]
@[simp]
theorem
WithBot.coe_biSup
{ι : Type u_5}
{s : Set ι}
(hs : s.Nonempty)
{α : Type u_6}
[CompleteLattice α]
(f : ι → α)
:
↑(⨆ i ∈ s, f i) = ⨆ i ∈ s, ↑(f i)
theorem
WithBot.coe_biInf
{ι : Type u_5}
{s : Set ι}
{α : Type u_6}
[CompleteLattice α]
(f : ι → α)
:
↑(⨅ i ∈ s, f i) = ⨅ i ∈ s, ↑(f i)
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
ciSup_le_iff
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{f : ι → α}
{a : α}
(hf : BddAbove (Set.range f))
:
theorem
le_ciInf_iff
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{f : ι → α}
{a : α}
(hf : BddBelow (Set.range f))
:
theorem
ciSup_set_le_iff
{α : Type u_1}
[ConditionallyCompleteLattice α]
{ι : Type u_5}
{s : Set ι}
{f : ι → α}
{a : α}
(hs : s.Nonempty)
(hf : BddAbove (f '' s))
:
theorem
le_ciInf_set_iff
{α : Type u_1}
[ConditionallyCompleteLattice α]
{ι : Type u_5}
{s : Set ι}
{f : ι → α}
{a : α}
(hs : s.Nonempty)
(hf : BddBelow (f '' s))
:
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
ciSup_le
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{f : ι → α}
{c : α}
(H : ∀ (x : ι), f x ≤ c)
:
The indexed supremum of a function is bounded above by a uniform bound
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
BddAbove.range_iSup_of_iUnion_range
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{κ : ι → Sort u_5}
{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
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
le_ciInf
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{f : ι → α}
{c : α}
(H : ∀ (x : ι), c ≤ f x)
:
The indexed minimum of a function is bounded below by a uniform lower bound
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
BddBelow.range_iInf_of_iUnion_range
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
{κ : ι → Sort u_5}
{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
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_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ConditionallyCompleteLattice α]
{f : β × γ → α}
(hf : BddAbove (Set.range f))
:
⨆ (p : β × γ), f p = ⨆ (b : β), ⨆ (c : γ), f (b, c)
theorem
ciInf_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ConditionallyCompleteLattice α]
{f : β × γ → α}
(hf : BddBelow (Set.range f))
:
⨅ (p : β × γ), f p = ⨅ (b : β), ⨅ (c : γ), f (b, c)
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
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
ciSup_subtype'
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{p : ι → Prop}
[Nonempty (Subtype p)]
{f : (i : ι) → p i → α}
(hf : BddAbove (Set.range fun (i : Subtype p) => f ↑i ⋯))
(hf' : sSup ∅ ≤ ⨆ (i : Subtype p), f ↑i ⋯)
:
⨆ (i : ι), ⨆ (h : p i), f i h = ⨆ (x : Subtype p), f ↑x ⋯
theorem
ciInf_subtype'
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLattice α]
[Nonempty ι]
{p : ι → Prop}
[Nonempty (Subtype p)]
{f : (i : ι) → p i → α}
(hf : BddBelow (Set.range fun (i : Subtype p) => f ↑i ⋯))
(hf' : ⨅ (i : Subtype p), f ↑i ⋯ ≤ sInf ∅)
:
⨅ (i : ι), ⨅ (h : p i), f i h = ⨅ (x : Subtype p), f ↑x ⋯
theorem
ciSup_subtype''
{α : Type u_1}
[ConditionallyCompleteLattice α]
{ι : Type u_5}
[Nonempty ι]
{s : Set ι}
(hs : s.Nonempty)
{f : ι → α}
(hf : BddAbove (Set.range fun (i : ↑s) => f ↑i))
(hf' : sSup ∅ ≤ ⨆ (i : ↑s), f ↑i)
:
⨆ (i : ↑s), f ↑i = ⨆ t ∈ s, f t
theorem
ciInf_subtype''
{α : Type u_1}
[ConditionallyCompleteLattice α]
{ι : Type u_5}
[Nonempty ι]
{s : Set ι}
(hs : s.Nonempty)
{f : ι → α}
(hf : BddBelow (Set.range fun (i : ↑s) => f ↑i))
(hf' : ⨅ (i : ↑s), f ↑i ≤ sInf ∅)
:
⨅ (i : ↑s), f ↑i = ⨅ t ∈ s, f t
theorem
ciSup_image
{α : Type u_5}
{ι : Type u_6}
{ι' : Type u_7}
[ConditionallyCompleteLattice α]
[Nonempty ι]
[Nonempty ι']
{s : Set ι}
(hs : s.Nonempty)
{f : ι → ι'}
{g : ι' → α}
(hf : BddAbove (Set.range fun (i : ↑s) => g (f ↑i)))
(hg' : sSup ∅ ≤ ⨆ (i : ↑s), g (f ↑i))
:
⨆ i ∈ f '' s, g i = ⨆ x ∈ s, g (f x)
theorem
ciInf_image
{α : Type u_5}
{ι : Type u_6}
{ι' : Type u_7}
[ConditionallyCompleteLattice α]
[Nonempty ι]
[Nonempty ι']
{s : Set ι}
(hs : s.Nonempty)
{f : ι → ι'}
{g : ι' → α}
(hf : BddBelow (Set.range fun (i : ↑s) => g (f ↑i)))
(hg' : ⨅ (i : ↑s), g (f ↑i) ≤ sInf ∅)
:
⨅ i ∈ f '' s, g i = ⨅ x ∈ s, g (f x)
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
lt_ciSup_iff
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
{a : α}
[Nonempty ι]
{f : ι → α}
(hb : BddAbove (Set.range f))
:
theorem
ciInf_lt_iff
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
{a : α}
[Nonempty ι]
{f : ι → α}
(hb : BddBelow (Set.range f))
:
theorem
cbiSup_eq_of_not_forall
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
{p : ι → Prop}
{f : Subtype p → α}
(hp : ¬∀ (i : ι), p i)
:
theorem
cbiInf_eq_of_not_forall
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
{p : ι → Prop}
{f : Subtype p → α}
(hp : ¬∀ (i : ι), p i)
:
theorem
ciInf_eq_bot_of_bot_mem
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
[OrderBot α]
{f : ι → α}
(hs : ⊥ ∈ Set.range f)
:
theorem
ciInf_eq_top_of_top_mem
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrder α]
[OrderTop α]
{f : ι → α}
(hs : ⊤ ∈ Set.range f)
:
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 : ι → α)
:
⨆ (i : ι), f i = ⊥
theorem
ciSup_false
{α : Type u_1}
[ConditionallyCompleteLinearOrderBot α]
(f : False → α)
:
⨆ (i : False), f i = ⊥
theorem
le_ciSup_iff'
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
{s : ι → α}
{a : α}
(h : BddAbove (Set.range s))
:
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
ciSup_or'
{α : Type u_1}
[ConditionallyCompleteLinearOrderBot α]
(p q : Prop)
(f : p ∨ q → α)
:
⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)
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)
:
l (sSup s) = ⨆ (x : ↑s), l ↑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.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)
:
u (sInf s) = ⨅ (x : ↑s), u ↑x
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)
:
e (sSup s) = ⨆ (x : ↑s), e ↑x
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)
:
e (sInf s) = ⨅ (x : ↑s), e ↑x
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)
@[simp]
theorem
OrderIso.map_ciSup'
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[ConditionallyCompleteLinearOrderBot α]
[ConditionallyCompleteLinearOrderBot β]
(e : α ≃o β)
(f : ι → α)
:
e (⨆ (i : ι), f i) = ⨆ (i : ι), e (f i)
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 : ι → α}
: