Conditionally complete lattices and finite sets. #

theorem Finset.Nonempty.csSup_eq_max' {α : Type u_2} {s : } (h : s.Nonempty) :
sSup s =
theorem Finset.Nonempty.csInf_eq_min' {α : Type u_2} {s : } (h : s.Nonempty) :
sInf s =
theorem Finset.Nonempty.csSup_mem {α : Type u_2} {s : } (h : s.Nonempty) :
sSup s s
theorem Finset.Nonempty.csInf_mem {α : Type u_2} {s : } (h : s.Nonempty) :
sInf s s
theorem Set.Nonempty.csSup_mem {α : Type u_2} {s : Set α} (h : ) (hs : ) :
sSup s s
theorem Set.Nonempty.csInf_mem {α : Type u_2} {s : Set α} (h : ) (hs : ) :
sInf s s
theorem Set.Finite.csSup_lt_iff {α : Type u_2} {s : Set α} {a : α} (hs : ) (h : ) :
sSup s < a xs, x < a
theorem Set.Finite.lt_csInf_iff {α : Type u_2} {s : Set α} {a : α} (hs : ) (h : ) :
a < sInf s xs, a < x

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} (s : ) (H : s.Nonempty) (f : ια) :
Finset.sup' s H f = sSup (f '' s)
theorem Finset.inf'_eq_csInf_image {ι : Type u_1} {α : Type u_2} (s : ) (H : s.Nonempty) (f : ια) :
Finset.inf' s H f = sInf (f '' s)
theorem Finset.sup'_id_eq_csSup {α : Type u_2} (s : ) (hs : s.Nonempty) :
Finset.sup' s hs id = sSup s
theorem Finset.inf'_id_eq_csInf {α : Type u_2} (s : ) (hs : s.Nonempty) :
Finset.inf' s hs id = sInf s
theorem Finset.sup'_univ_eq_ciSup {ι : Type u_1} {α : Type u_2} [] [] (f : ια) :
Finset.sup' Finset.univ f = ⨆ (i : ι), f i
theorem Finset.inf'_univ_eq_ciInf {ι : Type u_1} {α : Type u_2} [] [] (f : ια) :
Finset.inf' Finset.univ f = ⨅ (i : ι), f i
theorem Finset.sup_univ_eq_ciSup {ι : Type u_1} {α : Type u_2} [] (f : ια) :
Finset.sup Finset.univ f = ⨆ (i : ι), f i