Conditionally complete lattices and finite sets. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
finset.nonempty.sup'_eq_cSup_image
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{s : finset β}
(hs : s.nonempty)
(f : β → α) :
s.sup' hs f = has_Sup.Sup (f '' ↑s)
theorem
finset.nonempty.sup'_id_eq_cSup
{α : Type u_1}
[conditionally_complete_lattice α]
{s : finset α}
(hs : s.nonempty) :
s.sup' hs id = has_Sup.Sup ↑s
theorem
finset.nonempty.cSup_eq_max'
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : finset α}
(h : s.nonempty) :
has_Sup.Sup ↑s = s.max' h
theorem
finset.nonempty.cInf_eq_min'
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : finset α}
(h : s.nonempty) :
has_Inf.Inf ↑s = s.min' h
theorem
finset.nonempty.cSup_mem
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : finset α}
(h : s.nonempty) :
has_Sup.Sup ↑s ∈ s
theorem
finset.nonempty.cInf_mem
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : finset α}
(h : s.nonempty) :
has_Inf.Inf ↑s ∈ s
theorem
set.nonempty.cSup_mem
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : set α}
(h : s.nonempty)
(hs : s.finite) :
has_Sup.Sup s ∈ s
theorem
set.nonempty.cInf_mem
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : set α}
(h : s.nonempty)
(hs : s.finite) :
has_Inf.Inf s ∈ s
theorem
set.finite.cSup_lt_iff
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : set α}
{a : α}
(hs : s.finite)
(h : s.nonempty) :
theorem
set.finite.lt_cInf_iff
{α : Type u_1}
[conditionally_complete_linear_order α]
{s : set α}
{a : α}
(hs : s.finite)
(h : s.nonempty) :
Relation between Sup / Inf and finset.sup' / finset.inf' #
Like the Sup of a conditionally_complete_lattice, 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_1}
{β : Type u_2}
[conditionally_complete_lattice β]
(s : finset α)
(H : s.nonempty)
(f : α → β) :
s.sup' H f = has_Sup.Sup (f '' ↑s)
theorem
finset.inf'_eq_cInf_image
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice β]
(s : finset α)
(H : s.nonempty)
(f : α → β) :
s.inf' H f = has_Inf.Inf (f '' ↑s)
theorem
finset.sup'_id_eq_cSup
{α : Type u_1}
[conditionally_complete_lattice α]
(s : finset α)
(H : s.nonempty) :
s.sup' H id = has_Sup.Sup ↑s
theorem
finset.inf'_id_eq_cInf
{α : Type u_1}
[conditionally_complete_lattice α]
(s : finset α)
(H : s.nonempty) :
s.inf' H id = has_Inf.Inf ↑s