Documentation

Mathlib.Order.ConditionallyCompleteLattice.Finset

Conditionally complete lattices and finite sets. #

source
theorem ciSup_eq_ciSup_finset {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLattice α] [OrderBot α] [Nonempty ι] {a : ι → α} (ha : BddAbove (Set.range a)) :
⨆ (i : ι), a i = ⨆ (F : Finset ι), F.sup a

Supremum of a i, i : ι, is equal to the supremum over finite suprema of a.

source
theorem ciInf_eq_ciInf_finset {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLattice α] [OrderTop α] [Nonempty ι] {a : ι → α} (ha : BddBelow (Set.range a)) :
⨅ (i : ι), a i = ⨅ (F : Finset ι), F.inf a

Infimum of a i, i : ι, is equal to the infimum over finite infima of a.

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.Nonempty.isGreatest_csSup {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} (h : s.Nonempty) (hs : s.Finite) :
IsGreatest s (sSup s)
source
theorem Set.Nonempty.isLeast_csInf {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} (h : s.Nonempty) (hs : s.Finite) :
IsLeast s (sInf s)
source
theorem Finite.ciSup_mem {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] [Finite ι] (f : ι → α) :
⨆ (i : ι), f i ∈ Set.range f
source
theorem Finite.ciInf_mem {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] [Finite ι] (f : ι → α) :
⨅ (i : ι), f i ∈ Set.range f
source
theorem Finite.isGreatest_ciSup {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] [Finite ι] (f : ι → α) :
IsGreatest (Set.range f) (⨆ (i : ι), f i)
source
theorem Finite.isLeast_ciInf {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] [Finite ι] (f : ι → α) :
IsLeast (Set.range f) (⨅ (i : ι), f i)
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 Set.Finite.map_sSup_of_monotoneOn {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] {s : Set α} [ConditionallyCompletePartialOrderSup β] {f : α → β} (hfin : s.Finite) (hne : s.Nonempty) (hf : MonotoneOn f s) :
f (sSup s) = sSup (f '' s)
source
theorem Set.Finite.map_sInf_of_monotoneOn {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] {s : Set α} [ConditionallyCompletePartialOrderInf β] {f : α → β} (hfin : s.Finite) (hne : s.Nonempty) (hf : MonotoneOn f s) :
f (sInf s) = sInf (f '' s)
source
theorem Set.Finite.map_sSup_of_monotone {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] {s : Set α} [ConditionallyCompletePartialOrderSup β] {f : α → β} (hfin : s.Finite) (hne : s.Nonempty) (hf : Monotone f) :
f (sSup s) = sSup (f '' s)
source
theorem Set.Finite.map_sInf_of_monotone {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] {s : Set α} [ConditionallyCompletePartialOrderInf β] {f : α → β} (hfin : s.Finite) (hne : s.Nonempty) (hf : Monotone f) :
f (sInf s) = sInf (f '' s)
source
theorem Set.Finite.map_sSup_of_antitoneOn {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] {s : Set α} [ConditionallyCompletePartialOrder β] {f : α → β} (hfin : s.Finite) (hne : s.Nonempty) (hf : AntitoneOn f s) :
f (sSup s) = sInf (f '' s)
source
theorem Set.Finite.map_sInf_of_antitoneOn {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] {s : Set α} [ConditionallyCompletePartialOrder β] {f : α → β} (hfin : s.Finite) (hne : s.Nonempty) (hf : AntitoneOn f s) :
f (sInf s) = sSup (f '' s)
source
theorem Set.Finite.map_sSup_of_antitone {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] {s : Set α} [ConditionallyCompletePartialOrder β] {f : α → β} (hfin : s.Finite) (hne : s.Nonempty) (hf : Antitone f) :
f (sSup s) = sInf (f '' s)
source
theorem Set.Finite.map_sInf_of_antitone {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] {s : Set α} [ConditionallyCompletePartialOrder β] {f : α → β} (hfin : s.Finite) (hne : s.Nonempty) (hf : Antitone f) :
f (sInf s) = sSup (f '' s)
source
theorem Finset.ciSup_eq_max'_image {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Finset ι} (h : ∃ x ∈ s, sSup ∅ ≤ f x) (h' : (image f s).Nonempty := by exact image_nonempty.mpr (h.imp fun _ ↦ And.left)) :
⨆ i ∈ s, f i = (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' : (image f s).Nonempty := by exact image_nonempty.mpr (h.imp fun _ ↦ And.left)) :
⨅ i ∈ s, f i = (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 ∈ 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 ∈ 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 ∈ 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 ∈ 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 ∈ 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 ∈ 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
source
theorem sSup_ne_of_notMem {α : Type u_4} [CompleteLinearOrder α] {s : Set α} (hfin : s.Finite) {a : α} (hne : a ≠ ⊥) (hmem : a ∉ s) :
sSup s ≠ a
source
theorem sInf_ne_of_notMem {α : Type u_4} [CompleteLinearOrder α] {s : Set α} (hfin : s.Finite) {a : α} (hne : a ≠ ⊤) (hmem : a ∉ s) :
sInf s ≠ a
source
theorem sSup_ne_top {α : Type u_4} [CompleteLinearOrder α] [Nontrivial α] {s : Set α} (hfin : s.Finite) (htop : ⊤ ∉ s) :
sSup s ≠ ⊤
source
theorem sInf_ne_bot {α : Type u_4} [CompleteLinearOrder α] [Nontrivial α] {s : Set α} (hfin : s.Finite) (hbot : ⊥ ∉ s) :
sInf s ≠ ⊥
source
theorem iSup_ne_of_notMem {α : Type u_4} [CompleteLinearOrder α] {ι : Sort u_5} [Finite ι] {f : ι → α} {a : α} (hne : a ≠ ⊥) (h : ∀ (x : ι), f x ≠ a) :
iSup f ≠ a
source
theorem iInf_ne_of_notMem {α : Type u_4} [CompleteLinearOrder α] {ι : Sort u_5} [Finite ι] {f : ι → α} {a : α} (hne : a ≠ ⊤) (h : ∀ (x : ι), f x ≠ a) :
iInf f ≠ a
source
theorem iSup_ne_top {α : Type u_4} [CompleteLinearOrder α] {ι : Sort u_5} [Finite ι] [Nontrivial α] {f : ι → α} (h : ∀ (x : ι), f x ≠ ⊤) :
iSup f ≠ ⊤
source
theorem iInf_ne_bot {α : Type u_4} [CompleteLinearOrder α] {ι : Sort u_5} [Finite ι] [Nontrivial α] {f : ι → α} (h : ∀ (x : ι), f x ≠ ⊥) :
iInf f ≠ ⊥

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 : ι → α) :
univ.sup' ⋯ f = ⨆ (i : ι), f i
source
theorem Finset.inf'_univ_eq_ciInf {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLattice α] [Fintype ι] [Nonempty ι] (f : ι → α) :
univ.inf' ⋯ f = ⨅ (i : ι), f i
source
theorem Finset.sup_eq_ciSup {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] (s : Finset ι) (f : ι → α) :
s.sup f = ⨆ x ∈ s, f x
source
theorem Finset.sup_univ_eq_ciSup {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] [Fintype ι] (f : ι → α) :
univ.sup f = ⨆ (i : ι), f i
source
theorem Finset.ciSup_union {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] [DecidableEq ι] {f : ι → α} {s t : Finset ι} :
⨆ x ∈ s ∪ t, f x = max (⨆ x ∈ s, f x) (⨆ x ∈ t, f x)
source
theorem Finset.Nonempty.ciSup_eq_max'_image {ι : Type u_1} {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] (f : ι → α) {s : Finset ι} (h : s.Nonempty) (h' : (image f s).Nonempty := ⋯) :
⨆ i ∈ s, f i = (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 ∈ 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 ∈ 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 ∈ map f s