mathlib3 documentation

order.conditionally_complete_lattice.finset

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 set.nonempty.cSup_mem {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} (h : s.nonempty) (hs : s.finite) :
theorem set.nonempty.cInf_mem {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} (h : s.nonempty) (hs : s.finite) :
theorem set.finite.cSup_lt_iff {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} {a : α} (hs : s.finite) (h : s.nonempty) :
has_Sup.Sup s < a (x : α), x s x < a
theorem set.finite.lt_cInf_iff {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} {a : α} (hs : s.finite) (h : s.nonempty) :
a < has_Inf.Inf s (x : α), x s a < x

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)