Conditionally complete lattices and finite sets. #
theorem
Finset.Nonempty.sup'_eq_cSup_image
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{s : Finset β}
(hs : Finset.Nonempty s)
(f : β → α)
:
Finset.sup' s hs f = sSup (f '' ↑s)
theorem
Finset.Nonempty.sup'_id_eq_cSup
{α : Type u_1}
[ConditionallyCompleteLattice α]
{s : Finset α}
(hs : Finset.Nonempty s)
:
Finset.sup' s hs id = sSup ↑s
theorem
Finset.Nonempty.cSup_eq_max'
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : Finset.Nonempty s)
:
sSup ↑s = Finset.max' s h
theorem
Finset.Nonempty.cInf_eq_min'
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : Finset.Nonempty s)
:
sInf ↑s = Finset.min' s h
theorem
Finset.Nonempty.cSup_mem
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : Finset.Nonempty s)
:
theorem
Finset.Nonempty.cInf_mem
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : Finset.Nonempty s)
:
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_2}
[ConditionallyCompleteLattice β]
(s : Finset α)
(H : Finset.Nonempty s)
(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 : Finset.Nonempty s)
(f : α → β)
:
Finset.inf' s H f = sInf (f '' ↑s)
theorem
Finset.sup'_id_eq_csSup
{α : Type u_1}
[ConditionallyCompleteLattice α]
(s : Finset α)
(H : Finset.Nonempty s)
:
Finset.sup' s H id = sSup ↑s
theorem
Finset.inf'_id_eq_csInf
{α : Type u_1}
[ConditionallyCompleteLattice α]
(s : Finset α)
(H : Finset.Nonempty s)
:
Finset.inf' s H id = sInf ↑s