Conditionally complete lattices and finite sets. #
theorem
Finset.Nonempty.sup'_eq_cSup_image
{α : Type u_2}
{β : Type u_1}
[inst : ConditionallyCompleteLattice α]
{s : Finset β}
(hs : Finset.Nonempty s)
(f : β → α)
:
Finset.sup' s hs f = supₛ (f '' ↑s)
theorem
Finset.Nonempty.sup'_id_eq_cSup
{α : Type u_1}
[inst : ConditionallyCompleteLattice α]
{s : Finset α}
(hs : Finset.Nonempty s)
:
Finset.sup' s hs id = supₛ ↑s
theorem
Finset.Nonempty.cSup_eq_max'
{α : Type u_1}
[inst : ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : Finset.Nonempty s)
:
supₛ ↑s = Finset.max' s h
theorem
Finset.Nonempty.cInf_eq_min'
{α : Type u_1}
[inst : ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : Finset.Nonempty s)
:
infₛ ↑s = Finset.min' s h
theorem
Finset.Nonempty.cSup_mem
{α : Type u_1}
[inst : ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : Finset.Nonempty s)
:
theorem
Finset.Nonempty.cInf_mem
{α : Type u_1}
[inst : ConditionallyCompleteLinearOrder α]
{s : Finset α}
(h : Finset.Nonempty s)
:
theorem
Set.Nonempty.cSup_mem
{α : Type u_1}
[inst : ConditionallyCompleteLinearOrder α]
{s : Set α}
(h : Set.Nonempty s)
(hs : Set.Finite s)
:
theorem
Set.Nonempty.cInf_mem
{α : Type u_1}
[inst : ConditionallyCompleteLinearOrder α]
{s : Set α}
(h : Set.Nonempty s)
(hs : Set.Finite s)
:
theorem
Set.Finite.cSup_lt_iff
{α : Type u_1}
[inst : ConditionallyCompleteLinearOrder α]
{s : Set α}
{a : α}
(hs : Set.Finite s)
(h : Set.Nonempty s)
:
theorem
Set.Finite.lt_cInf_iff
{α : Type u_1}
[inst : 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_csupₛ_image
{α : Type u_2}
{β : Type u_1}
[inst : ConditionallyCompleteLattice β]
(s : Finset α)
(H : Finset.Nonempty s)
(f : α → β)
:
Finset.sup' s H f = supₛ (f '' ↑s)
theorem
Finset.inf'_eq_cinfₛ_image
{α : Type u_2}
{β : Type u_1}
[inst : ConditionallyCompleteLattice β]
(s : Finset α)
(H : Finset.Nonempty s)
(f : α → β)
:
Finset.inf' s H f = infₛ (f '' ↑s)
theorem
Finset.sup'_id_eq_csupₛ
{α : Type u_1}
[inst : ConditionallyCompleteLattice α]
(s : Finset α)
(H : Finset.Nonempty s)
:
Finset.sup' s H id = supₛ ↑s
theorem
Finset.inf'_id_eq_cinfₛ
{α : Type u_1}
[inst : ConditionallyCompleteLattice α]
(s : Finset α)
(H : Finset.Nonempty s)
:
Finset.inf' s H id = infₛ ↑s