Conditionally complete lattices and finite sets. #
theorem
Finset.Nonempty.sup'_eq_cSup_image
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{s : Finset β}
(hs : s.Nonempty)
(f : β → α)
:
Finset.sup' s hs f = sSup (f '' ↑s)
theorem
Finset.Nonempty.sup'_id_eq_cSup
{α : Type u_1}
[ConditionallyCompleteLattice α]
{s : Finset α}
(hs : s.Nonempty)
:
Finset.sup' s hs id = sSup ↑s
theorem
Finset.Nonempty.cSup_eq_max'
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : s.Nonempty)
:
sSup ↑s = Finset.max' s h
theorem
Finset.Nonempty.cInf_eq_min'
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : s.Nonempty)
:
sInf ↑s = Finset.min' s h
theorem
Finset.Nonempty.cSup_mem
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : s.Nonempty)
:
theorem
Finset.Nonempty.cInf_mem
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : s.Nonempty)
:
theorem
Set.Nonempty.cSup_mem
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
(h : Set.Nonempty s)
(hs : Set.Finite s)
:
theorem
Set.Nonempty.cInf_mem
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
(h : Set.Nonempty s)
(hs : Set.Finite s)
:
theorem
Set.Finite.cSup_lt_iff
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
{a : α}
(hs : Set.Finite s)
(h : Set.Nonempty s)
:
theorem
Set.Finite.lt_cInf_iff
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
{a : α}
(hs : Set.Finite s)
(h : Set.Nonempty s)
:
Relation between Sup / Inf and Finset.sup' / Finset.inf' #
Like the Sup of a ConditionallyCompleteLattice, Finset.sup' also requires the set to be
non-empty. As a result, we can translate between the two.
theorem
Finset.sup'_eq_csSup_image
{α : Type u_1}
{ι : Type u_4}
[ConditionallyCompleteLattice α]
(s : Finset ι)
(H : s.Nonempty)
(f : ι → α)
:
Finset.sup' s H f = sSup (f '' ↑s)
theorem
Finset.inf'_eq_csInf_image
{α : Type u_1}
{ι : Type u_4}
[ConditionallyCompleteLattice α]
(s : Finset ι)
(hs : s.Nonempty)
(f : ι → α)
:
Finset.inf' s hs f = sInf (f '' ↑s)
theorem
Finset.sup'_id_eq_csSup
{α : Type u_1}
[ConditionallyCompleteLattice α]
(s : Finset α)
(hs : s.Nonempty)
:
Finset.sup' s hs id = sSup ↑s
theorem
Finset.inf'_id_eq_csInf
{α : Type u_1}
[ConditionallyCompleteLattice α]
(s : Finset α)
(hs : s.Nonempty)
:
Finset.inf' s hs id = sInf ↑s
theorem
Finset.sup'_univ_eq_ciSup
{α : Type u_1}
{ι : Type u_4}
[ConditionallyCompleteLattice α]
[Fintype ι]
[Nonempty ι]
(f : ι → α)
:
Finset.sup' Finset.univ (_ : Finset.univ.Nonempty) f = ⨆ (i : ι), f i
theorem
Finset.inf'_univ_eq_ciInf
{α : Type u_1}
{ι : Type u_4}
[ConditionallyCompleteLattice α]
[Fintype ι]
[Nonempty ι]
(f : ι → α)
:
Finset.inf' Finset.univ (_ : Finset.univ.Nonempty) f = ⨅ (i : ι), f i