Documentation

Mathlib.Order.ConditionallyCompleteLattice.Finset

Conditionally complete lattices and finite sets. #

source
theorem Finset.Nonempty.csSup_eq_max' {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Finset α} (h : s.Nonempty) :
sSup ↑s = s.max' h
source
theorem Finset.Nonempty.csInf_eq_min' {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Finset α} (h : s.Nonempty) :
sInf ↑s = s.min' h
source
theorem Finset.Nonempty.csSup_mem {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Finset α} (h : s.Nonempty) :
sSup ↑s ∈ s
source
theorem Finset.Nonempty.csInf_mem {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Finset α} (h : s.Nonempty) :
sInf ↑s ∈ s
source
theorem Set.Nonempty.csSup_mem {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} (h : s.Nonempty) (hs : s.Finite) :
sSup s ∈ s
source
theorem Set.Nonempty.csInf_mem {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} (h : s.Nonempty) (hs : s.Finite) :
sInf s ∈ s
source
theorem Set.Finite.csSup_lt_iff {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} {a : α} (hs : s.Finite) (h : s.Nonempty) :
sSup s < a ↔ ∀ x ∈ s, x < a
source
theorem Set.Finite.lt_csInf_iff {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} {a : α} (hs : s.Finite) (h : s.Nonempty) :
a < sInf s ↔ ∀ x ∈ s, 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.

source
theorem Finset.sup'_eq_csSup_image {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLattice α] (s : Finset ι) (H : s.Nonempty) (f : ι → α) :
s.sup' H f = sSup (f '' ↑s)
source
theorem Finset.inf'_eq_csInf_image {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLattice α] (s : Finset ι) (H : s.Nonempty) (f : ι → α) :
s.inf' H f = sInf (f '' ↑s)
source
theorem Finset.sup'_id_eq_csSup {α : Type u_2} [ConditionallyCompleteLattice α] (s : Finset α) (hs : s.Nonempty) :
s.sup' hs id = sSup ↑s
source
theorem Finset.inf'_id_eq_csInf {α : Type u_2} [ConditionallyCompleteLattice α] (s : Finset α) (hs : s.Nonempty) :
s.inf' hs id = sInf ↑s
source
theorem Finset.sup'_univ_eq_ciSup {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLattice α] [Fintype ι] [Nonempty ι] (f : ι → α) :
Finset.univ.sup' ⋯ f = ⨆ (i : ι), f i
source
theorem Finset.inf'_univ_eq_ciInf {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLattice α] [Fintype ι] [Nonempty ι] (f : ι → α) :
Finset.univ.inf' ⋯ f = ⨅ (i : ι), f i
source
theorem Finset.sup_univ_eq_ciSup {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] [Fintype ι] (f : ι → α) :
Finset.univ.sup f = ⨆ (i : ι), f i