Conditionally complete lattices and finite sets. #
theorem
Finset.Nonempty.csSup_eq_max'
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : s.Nonempty)
:
sSup ↑s = Finset.max' s h
theorem
Finset.Nonempty.csInf_eq_min'
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : s.Nonempty)
:
sInf ↑s = Finset.min' s h
theorem
Finset.Nonempty.csSup_mem
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : s.Nonempty)
:
theorem
Finset.Nonempty.csInf_mem
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : s.Nonempty)
:
theorem
Set.Nonempty.csSup_mem
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
(h : Set.Nonempty s)
(hs : Set.Finite s)
:
theorem
Set.Nonempty.csInf_mem
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
(h : Set.Nonempty s)
(hs : Set.Finite s)
:
theorem
Set.Finite.csSup_lt_iff
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
{a : α}
(hs : Set.Finite s)
(h : Set.Nonempty s)
:
theorem
Set.Finite.lt_csInf_iff
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
{s : Set α}
{a : α}
(hs : Set.Finite s)
(h : Set.Nonempty s)
:
Relation between sSup / sInf 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_2}
[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_2}
[ConditionallyCompleteLattice α]
(s : Finset ι)
(H : s.Nonempty)
(f : ι → α)
:
Finset.inf' s H f = sInf (f '' ↑s)
theorem
Finset.sup'_id_eq_csSup
{α : Type u_2}
[ConditionallyCompleteLattice α]
(s : Finset α)
(hs : s.Nonempty)
:
Finset.sup' s hs id = sSup ↑s
theorem
Finset.inf'_id_eq_csInf
{α : Type u_2}
[ConditionallyCompleteLattice α]
(s : Finset α)
(hs : s.Nonempty)
:
Finset.inf' s hs id = sInf ↑s
theorem
Finset.sup'_univ_eq_ciSup
{ι : Type u_1}
{α : Type u_2}
[ConditionallyCompleteLattice α]
[Fintype ι]
[Nonempty ι]
(f : ι → α)
:
Finset.sup' Finset.univ ⋯ f = ⨆ (i : ι), f i
theorem
Finset.inf'_univ_eq_ciInf
{ι : Type u_1}
{α : Type u_2}
[ConditionallyCompleteLattice α]
[Fintype ι]
[Nonempty ι]
(f : ι → α)
:
Finset.inf' Finset.univ ⋯ f = ⨅ (i : ι), f i
theorem
Finset.sup_univ_eq_ciSup
{ι : Type u_1}
{α : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
[Fintype ι]
(f : ι → α)
:
Finset.sup Finset.univ f = ⨆ (i : ι), f i