HepLean 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
source
theorem Finset.ciSup_eq_max'_image {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Finset ι} (h : ∃ x ∈ s, sSup ∅ ≤ f x) (h' : (Finset.image f s).Nonempty := by classical exact image_nonempty.mpr (h.imp fun _ ↦ And.left)) :
⨆ i ∈ s, f i = (Finset.image f s).max' h'
source
theorem Finset.ciInf_eq_min'_image {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Finset ι} (h : ∃ x ∈ s, f x ≤ sInf ∅) (h' : (Finset.image f s).Nonempty := by classical exact image_nonempty.mpr (h.imp fun _ ↦ And.left)) :
⨅ i ∈ s, f i = (Finset.image f s).min' h'
source
theorem Finset.ciSup_mem_image {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Finset ι} (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
⨆ i ∈ s, f i ∈ Finset.image f s
source
theorem Finset.ciInf_mem_image {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Finset ι} (h : ∃ x ∈ s, f x ≤ sInf ∅) :
⨅ i ∈ s, f i ∈ Finset.image f s
source
theorem Set.Finite.ciSup_mem_image {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Set ι} (hs : s.Finite) (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
⨆ i ∈ s, f i ∈ f '' s
source
theorem Set.Finite.ciInf_mem_image {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Set ι} (hs : s.Finite) (h : ∃ x ∈ s, f x ≤ sInf ∅) :
⨅ i ∈ s, f i ∈ f '' s
source
theorem Set.Finite.ciSup_lt_iff {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] {a : α} {s : Set ι} {f : ι → α} (hs : s.Finite) (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a
source
theorem Set.Finite.lt_ciInf_iff {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] {a : α} {s : Set ι} {f : ι → α} (hs : s.Finite) (h : ∃ x ∈ s, f x ≤ sInf ∅) :
a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x
source
theorem List.iSup_mem_map_of_exists_sSup_empty_le {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] {l : List ι} (f : ι → α) (h : ∃ x ∈ l, sSup ∅ ≤ f x) :
⨆ x ∈ l, f x ∈ List.map f l
source
theorem List.iInf_mem_map_of_exists_le_sInf_empty {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] {l : List ι} (f : ι → α) (h : ∃ x ∈ l, f x ≤ sInf ∅) :
⨅ x ∈ l, f x ∈ List.map f l
source
theorem Multiset.iSup_mem_map_of_exists_sSup_empty_le {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Multiset ι} (f : ι → α) (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
⨆ x ∈ s, f x ∈ Multiset.map f s
source
theorem Multiset.iInf_mem_map_of_exists_le_sInf_empty {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Multiset ι} (f : ι → α) (h : ∃ x ∈ s, f x ≤ sInf ∅) :
⨅ x ∈ s, f x ∈ Multiset.map f s
source
theorem exists_eq_ciSup_of_finite {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] [Finite ι] {f : ι → α} :
∃ (i : ι), f i = ⨆ (i : ι), f i
source
theorem exists_eq_ciInf_of_finite {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] [Finite ι] {f : ι → α} :
∃ (i : ι), f i = ⨅ (i : ι), f i

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
source
theorem Finset.Nonempty.ciSup_eq_max'_image {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] (f : ι → α) {s : Finset ι} (h : s.Nonempty) (h' : (Finset.image f s).Nonempty := ⋯) :
⨆ i ∈ s, f i = (Finset.image f s).max' h'
source
theorem Finset.Nonempty.ciSup_mem_image {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] (f : ι → α) {s : Finset ι} (h : s.Nonempty) :
⨆ i ∈ s, f i ∈ Finset.image f s
source
theorem Set.Nonempty.ciSup_mem_image {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] (f : ι → α) {s : Set ι} (h : s.Nonempty) (hs : s.Finite) :
⨆ i ∈ s, f i ∈ f '' s
source
theorem Set.Nonempty.ciSup_lt_iff {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {s : Set ι} {a : α} {f : ι → α} (h : s.Nonempty) (hs : s.Finite) :
⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a
source
theorem List.iSup_mem_map_of_ne_nil {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {l : List ι} (f : ι → α) (h : l ≠ []) :
⨆ x ∈ l, f x ∈ List.map f l
source
theorem Multiset.iSup_mem_map_of_ne_zero {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {s : Multiset ι} (f : ι → α) (h : s ≠ 0) :
⨆ x ∈ s, f x ∈ Multiset.map f s