Mathlib.Order.ConditionallyCompleteLattice.Finset

Finset.Nonempty.csSup_eq_max' theorem

{s : Finset α} (h : s.Nonempty) : sSup ↑s = s.max' h

Full source

theorem Finset.Nonempty.csSup_eq_max' {s : Finset α} (h : s.Nonempty) : sSup ↑s = s.max' h :=
  eq_of_forall_ge_iff fun _ => (csSup_le_iff s.bddAbove h.to_set).trans (s.max'_le_iff h).symm

Supremum of Nonempty Finite Set Equals Maximum Element

Informal description

For any nonempty finite set $s$ in a conditionally complete linear order $\alpha$, the supremum of $s$ (as a subset of $\alpha$) is equal to the maximum element of $s$, i.e., \[ \sup s = \max' s, \] where $\max' s$ denotes the maximum element of $s$ (which exists since $s$ is nonempty and finite).

Finset.Nonempty.csInf_eq_min' theorem

{s : Finset α} (h : s.Nonempty) : sInf ↑s = s.min' h

Full source

theorem Finset.Nonempty.csInf_eq_min' {s : Finset α} (h : s.Nonempty) : sInf ↑s = s.min' h :=
  @Finset.Nonempty.csSup_eq_max' αᵒᵈ _ s h

Infimum of Nonempty Finite Set Equals Minimum Element

Informal description

For any nonempty finite set $s$ in a conditionally complete linear order $\alpha$, the infimum of $s$ (as a subset of $\alpha$) is equal to the minimum element of $s$, i.e., \[ \inf s = \min' s, \] where $\min' s$ denotes the minimum element of $s$ (which exists since $s$ is nonempty and finite).

Finset.Nonempty.csSup_mem theorem

{s : Finset α} (h : s.Nonempty) : sSup (s : Set α) ∈ s

Full source

theorem Finset.Nonempty.csSup_mem {s : Finset α} (h : s.Nonempty) : sSupsSup (s : Set α) ∈ s := by
  rw [h.csSup_eq_max']
  exact s.max'_mem _

Supremum of Nonempty Finite Set Belongs to the Set

Informal description

For any nonempty finite set $s$ in a conditionally complete linear order $\alpha$, the supremum of $s$ (as a subset of $\alpha$) is an element of $s$, i.e., \[ \sup s \in s. \]

Finset.Nonempty.csInf_mem theorem

{s : Finset α} (h : s.Nonempty) : sInf (s : Set α) ∈ s

Full source

theorem Finset.Nonempty.csInf_mem {s : Finset α} (h : s.Nonempty) : sInfsInf (s : Set α) ∈ s :=
  @Finset.Nonempty.csSup_mem αᵒᵈ _ _ h

Infimum of Nonempty Finite Set Belongs to the Set

Informal description

For any nonempty finite set $s$ in a conditionally complete linear order $\alpha$, the infimum of $s$ (as a subset of $\alpha$) is an element of $s$, i.e., \[ \inf s \in s. \]

Set.Nonempty.csSup_mem theorem

(h : s.Nonempty) (hs : s.Finite) : sSup s ∈ s

Full source

theorem Set.Nonempty.csSup_mem (h : s.Nonempty) (hs : s.Finite) : sSupsSup s ∈ s := by
  lift s to Finset α using hs
  exact Finset.Nonempty.csSup_mem h

Supremum of Nonempty Finite Set Belongs to the Set

Informal description

For any nonempty finite subset $s$ of a conditionally complete linear order $\alpha$, the supremum of $s$ is an element of $s$, i.e., \[ \sup s \in s. \]

Set.Nonempty.csInf_mem theorem

(h : s.Nonempty) (hs : s.Finite) : sInf s ∈ s

Full source

theorem Set.Nonempty.csInf_mem (h : s.Nonempty) (hs : s.Finite) : sInfsInf s ∈ s :=
  @Set.Nonempty.csSup_mem αᵒᵈ _ _ h hs

Infimum of Nonempty Finite Set Belongs to the Set

Informal description

For any nonempty finite subset $s$ of a conditionally complete linear order $\alpha$, the infimum of $s$ is an element of $s$, i.e., \[ \inf s \in s. \]

Set.Finite.csSup_lt_iff theorem

(hs : s.Finite) (h : s.Nonempty) : sSup s < a ↔ ∀ x ∈ s, x < a

Full source

theorem Set.Finite.csSup_lt_iff (hs : s.Finite) (h : s.Nonempty) : sSupsSup s < a ↔ ∀ x ∈ s, x < a :=
  ⟨fun h _ hx => (le_csSup hs.bddAbove hx).trans_lt h, fun H => H _ <| h.csSup_mem hs⟩

Supremum of Finite Set is Less Than iff All Elements Are Less Than

Informal description

Let $s$ be a nonempty finite subset of a conditionally complete linear order $\alpha$, and let $a \in \alpha$. The supremum of $s$ is strictly less than $a$ if and only if every element $x \in s$ satisfies $x < a$. In other words, \[ \sup s < a \leftrightarrow \forall x \in s, x < a. \]

Set.Finite.lt_csInf_iff theorem

(hs : s.Finite) (h : s.Nonempty) : a < sInf s ↔ ∀ x ∈ s, a < x

Full source

theorem Set.Finite.lt_csInf_iff (hs : s.Finite) (h : s.Nonempty) : a < sInf s ↔ ∀ x ∈ s, a < x :=
  @Set.Finite.csSup_lt_iff αᵒᵈ _ _ _ hs h

Characterization of Elements Below Infimum in Finite Sets

Informal description

Let $s$ be a nonempty finite subset of a conditionally complete linear order $\alpha$, and let $a \in \alpha$. Then $a$ is strictly less than the infimum of $s$ if and only if $a$ is strictly less than every element $x \in s$. In other words, \[ a < \inf s \leftrightarrow \forall x \in s, a < x. \]

Finset.ciSup_mem_image theorem

{s : Finset ι} (h : ∃ x ∈ s, sSup ∅ ≤ f x) : ⨆ i ∈ s, f i ∈ s.image f

Full source

theorem Finset.ciSup_mem_image {s : Finset ι} (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
    ⨆ i ∈ s, f i⨆ i ∈ s, f i ∈ s.image f := by
  rw [ciSup_eq_max'_image _ h]
  exact max'_mem (image f s) _

Supremum of Function over Finite Set Belongs to Its Image

Informal description

Let $s$ be a finite set (finset) of elements of type $\iota$, and let $f$ be a function defined on $\iota$. If there exists an element $x \in s$ such that the supremum of the empty set is less than or equal to $f(x)$, then the supremum of $f$ over $s$ is an element of the image of $s$ under $f$. In other words, $\bigsqcup_{i \in s} f(i) \in f(s)$.

Finset.ciInf_mem_image theorem

{s : Finset ι} (h : ∃ x ∈ s, f x ≤ sInf ∅) : ⨅ i ∈ s, f i ∈ s.image f

Full source

theorem Finset.ciInf_mem_image {s : Finset ι} (h : ∃ x ∈ s, f x ≤ sInf ∅) :
    ⨅ i ∈ s, f i⨅ i ∈ s, f i ∈ s.image f := by
  rw [ciInf_eq_min'_image _ h]
  exact min'_mem (image f s) _

Infimum of Function over Finite Set Belongs to Its Image

Informal description

Let $s$ be a finite set (finset) of elements of type $\iota$, and let $f : \iota \to \alpha$ be a function where $\alpha$ is a conditionally complete linear order. If there exists an element $x \in s$ such that $f(x) \leq \inf \emptyset$, then the infimum of $f$ over $s$ belongs to the image of $s$ under $f$, i.e., $\bigsqcap_{i \in s} f(i) \in f(s)$.

Set.Finite.ciSup_mem_image theorem

{s : Set ι} (hs : s.Finite) (h : ∃ x ∈ s, sSup ∅ ≤ f x) : ⨆ i ∈ s, f i ∈ f '' s

Full source

theorem Set.Finite.ciSup_mem_image {s : Set ι} (hs : s.Finite) (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
    ⨆ i ∈ s, f i⨆ i ∈ s, f i ∈ f '' s := by
  lift s to Finset ι using hs
  simp only [Finset.mem_coe] at h
  simpa using Finset.ciSup_mem_image f h

Supremum of Function over Finite Set Belongs to Its Image

Informal description

Let $s$ be a finite set of elements of type $\iota$, and let $f : \iota \to \alpha$ be a function where $\alpha$ is a conditionally complete linear order. If there exists an element $x \in s$ such that the supremum of the empty set is less than or equal to $f(x)$, then the supremum of $f$ over $s$ belongs to the image of $s$ under $f$, i.e., $\bigsqcup_{i \in s} f(i) \in f(s)$.

Set.Finite.ciInf_mem_image theorem

{s : Set ι} (hs : s.Finite) (h : ∃ x ∈ s, f x ≤ sInf ∅) : ⨅ i ∈ s, f i ∈ f '' s

Full source

theorem Set.Finite.ciInf_mem_image {s : Set ι} (hs : s.Finite) (h : ∃ x ∈ s, f x ≤ sInf ∅) :
    ⨅ i ∈ s, f i⨅ i ∈ s, f i ∈ f '' s := by
  lift s to Finset ι using hs
  simp only [Finset.mem_coe] at h
  simpa using Finset.ciInf_mem_image f h

Infimum of Function over Finite Set Belongs to Its Image

Informal description

Let $s$ be a finite set of elements of type $\iota$, and let $f : \iota \to \alpha$ be a function where $\alpha$ is a conditionally complete linear order. If there exists an element $x \in s$ such that $f(x) \leq \inf \emptyset$, then the infimum of $f$ over $s$ belongs to the image of $s$ under $f$, i.e., $\bigsqcap_{i \in s} f(i) \in f(s)$.

Set.Finite.ciSup_lt_iff theorem

 {s : Set ι} {f : ι → α} (hs : s.Finite) (h : ∃ x ∈ s, sSup ∅ ≤ f x) : ⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a

Full source

theorem Set.Finite.ciSup_lt_iff {s : Set ι} {f : ι → α} (hs : s.Finite)
    (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
    ⨆ i ∈ s, f i⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a := by
  constructor
  · intro h x hx
    refine h.trans_le' (le_csSup ?_ ?_)
    · classical
      refine (((hs.image f).union (finite_singleton (sSup ∅))).subset ?_).bddAbove
      intro
      simp only [ciSup_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
      intro x hx
      split_ifs at hx
      · exact Or.inr ⟨_, by assumption, hx⟩
      · simp_all
    · simp only [mem_range]
      refine ⟨x, ?_⟩
      simp [hx]
  · intro H
    have := hs.ciSup_mem_image _ h
    simp only [mem_image] at this
    obtain ⟨_, hmem, hx⟩ := this
    rw [← hx]
    exact H _ hmem

Supremum over Finite Set is Less Than iff All Elements Are Less Than

Informal description

Let $s$ be a finite subset of a type $\iota$, and let $f : \iota \to \alpha$ be a function where $\alpha$ is a conditionally complete linear order. Suppose there exists an element $x \in s$ such that the supremum of the empty set is less than or equal to $f(x)$. Then the supremum of $f$ over $s$ is less than a value $a$ if and only if $f(x) < a$ for all $x \in s$. In other words: \[ \bigsqcup_{i \in s} f(i) < a \leftrightarrow \forall x \in s, f(x) < a. \]

Set.Finite.lt_ciInf_iff theorem

 {s : Set ι} {f : ι → α} (hs : s.Finite) (h : ∃ x ∈ s, f x ≤ sInf ∅) : a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x

Full source

theorem Set.Finite.lt_ciInf_iff {s : Set ι} {f : ι → α} (hs : s.Finite)
    (h : ∃ x ∈ s, f x ≤ sInf ∅) :
    a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x := by
  constructor
  · intro h x hx
    refine h.trans_le (csInf_le ?_ ?_)
    · classical
      refine (((hs.image f).union (finite_singleton (sInf ∅))).subset ?_).bddBelow
      intro
      simp only [ciInf_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
      intro x hx
      split_ifs at hx
      · exact Or.inr ⟨_, by assumption, hx⟩
      · simp_all
    · simp only [mem_range]
      refine ⟨x, ?_⟩
      simp [hx]
  · intro H
    have := hs.ciInf_mem_image _ h
    simp only [mem_image] at this
    obtain ⟨_, hmem, hx⟩ := this
    rw [← hx]
    exact H _ hmem

Characterization of Strictly Below Infimum in Finite Sets

Informal description

Let $s$ be a finite subset of a type $\iota$, and let $f : \iota \to \alpha$ be a function where $\alpha$ is a conditionally complete linear order. Suppose there exists an element $x \in s$ such that $f(x) \leq \inf \emptyset$. Then for any element $a \in \alpha$, we have: \[ a < \bigsqcap_{i \in s} f(i) \leftrightarrow \forall x \in s, a < f(x). \]

List.iSup_mem_map_of_exists_sSup_empty_le theorem

{l : List ι} (f : ι → α) (h : ∃ x ∈ l, sSup ∅ ≤ f x) : ⨆ x ∈ l, f x ∈ l.map f

Full source

lemma List.iSup_mem_map_of_exists_sSup_empty_le {l : List ι} (f : ι → α)
    (h : ∃ x ∈ l, sSup ∅ ≤ f x) :
    ⨆ x ∈ l, f x⨆ x ∈ l, f x ∈ l.map f := by
  classical
  simpa using l.toFinset.ciSup_mem_image f (by simpa using h)

Supremum of Function over List Belongs to Its Image

Informal description

Let $l$ be a list of elements of type $\iota$, and let $f : \iota \to \alpha$ be a function where $\alpha$ is a conditionally complete linear order. If there exists an element $x \in l$ such that the supremum of the empty set is less than or equal to $f(x)$, then the supremum of $f$ over the list $l$ is an element of the image of $l$ under $f$. In other words, $\bigsqcup_{x \in l} f(x) \in f(l)$.

List.iInf_mem_map_of_exists_le_sInf_empty theorem

{l : List ι} (f : ι → α) (h : ∃ x ∈ l, f x ≤ sInf ∅) : ⨅ x ∈ l, f x ∈ l.map f

Full source

lemma List.iInf_mem_map_of_exists_le_sInf_empty {l : List ι} (f : ι → α)
    (h : ∃ x ∈ l, f x ≤ sInf ∅) :
    ⨅ x ∈ l, f x⨅ x ∈ l, f x ∈ l.map f := by
  classical
  simpa using l.toFinset.ciInf_mem_image f (by simpa using h)

Infimum of Function over List Belongs to Its Image When Bounded Above by Empty Infimum

Informal description

Let $\alpha$ be a conditionally complete linear order, $l$ be a list of elements of type $\iota$, and $f : \iota \to \alpha$ be a function. If there exists an element $x \in l$ such that $f(x) \leq \inf \emptyset$, then the infimum of $f$ over the list $l$ is an element of the image of $l$ under $f$, i.e., $\bigsqcap_{x \in l} f(x) \in f(l)$.

Multiset.iSup_mem_map_of_exists_sSup_empty_le theorem

{s : Multiset ι} (f : ι → α) (h : ∃ x ∈ s, sSup ∅ ≤ f x) : ⨆ x ∈ s, f x ∈ s.map f

Full source

lemma Multiset.iSup_mem_map_of_exists_sSup_empty_le {s : Multiset ι} (f : ι → α)
    (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
    ⨆ x ∈ s, f x⨆ x ∈ s, f x ∈ s.map f := by
  classical
  simpa using s.toFinset.ciSup_mem_image f (by simpa using h)

Supremum of Function over Multiset Belongs to Its Image When Bounded Below by Empty Supremum

Informal description

Let $s$ be a multiset of elements of type $\iota$ in a conditionally complete linear order $\alpha$, and let $f : \iota \to \alpha$ be a function. If there exists an element $x \in s$ such that the supremum of the empty set is less than or equal to $f(x)$, then the supremum of $f$ over all elements in $s$ belongs to the image of $s$ under $f$. In other words, $\bigsqcup_{x \in s} f(x) \in f(s)$.

Multiset.iInf_mem_map_of_exists_le_sInf_empty theorem

{s : Multiset ι} (f : ι → α) (h : ∃ x ∈ s, f x ≤ sInf ∅) : ⨅ x ∈ s, f x ∈ s.map f

Full source

lemma Multiset.iInf_mem_map_of_exists_le_sInf_empty {s : Multiset ι} (f : ι → α)
    (h : ∃ x ∈ s, f x ≤ sInf ∅) :
    ⨅ x ∈ s, f x⨅ x ∈ s, f x ∈ s.map f := by
  classical
  simpa using s.toFinset.ciInf_mem_image f (by simpa using h)

Infimum of Function over Multiset Belongs to Its Image When Bounded Below by Empty Infimum

Informal description

Let $\alpha$ be a conditionally complete linear order, $s$ be a multiset of elements of type $\iota$, and $f : \iota \to \alpha$ be a function. If there exists an element $x \in s$ such that $f(x) \leq \inf \emptyset$, then the infimum of $f$ over all elements in $s$ belongs to the image of $s$ under $f$, i.e., \[ \inf_{x \in s} f(x) \in f(s). \]

exists_eq_ciSup_of_finite theorem

[Nonempty ι] [Finite ι] {f : ι → α} : ∃ i, f i = ⨆ i, f i

Full source

theorem exists_eq_ciSup_of_finite [Nonempty ι] [Finite ι] {f : ι → α} : ∃ i, f i = ⨆ i, f i :=
  Nonempty.csSup_mem (range_nonempty f) (finite_range f)

Existence of Attained Supremum for Finite Nonempty Domains in Conditionally Complete Linear Orders

Informal description

Let $\alpha$ be a conditionally complete linear order, and let $\iota$ be a nonempty finite type. For any function $f : \iota \to \alpha$, there exists an index $i \in \iota$ such that $f(i)$ equals the supremum of $f$ over all indices in $\iota$, i.e., \[ \exists i \in \iota, \quad f(i) = \sup_{j \in \iota} f(j). \]

exists_eq_ciInf_of_finite theorem

[Nonempty ι] [Finite ι] {f : ι → α} : ∃ i, f i = ⨅ i, f i

Full source

theorem exists_eq_ciInf_of_finite [Nonempty ι] [Finite ι] {f : ι → α} : ∃ i, f i = ⨅ i, f i :=
  Nonempty.csInf_mem (range_nonempty f) (finite_range f)

Existence of Attained Infimum for Finite Nonempty Domains in Conditionally Complete Linear Orders

Informal description

Let $\alpha$ be a conditionally complete linear order and $\iota$ be a nonempty finite type. For any function $f : \iota \to \alpha$, there exists an index $i \in \iota$ such that $f(i)$ equals the infimum of $f$ over all indices in $\iota$, i.e., \[ \exists i \in \iota, \quad f(i) = \inf_{j \in \iota} f(j). \]

Finset.sup'_eq_csSup_image theorem

(s : Finset ι) (H : s.Nonempty) (f : ι → α) : s.sup' H f = sSup (f '' s)

Full source

theorem sup'_eq_csSup_image (s : Finset ι) (H : s.Nonempty) (f : ι → α) :
    s.sup' H f = sSup (f '' s) :=
  eq_of_forall_ge_iff fun a => by
    simp [csSup_le_iff (s.finite_toSet.image f).bddAbove (H.to_set.image f)]

Equality of Finite Supremum and Image Supremum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, $s$ a nonempty finite set of type $\iota$, and $f : \iota \to \alpha$ a function. Then the supremum of $f$ over $s$ (denoted $s.\text{sup}'\, H\, f$) is equal to the supremum of the image of $f$ over $s$ (denoted $\sup (f \,''\, s)$). In other words: \[ \sup_{i \in s} f(i) = \sup \{ f(i) \mid i \in s \}. \]

Finset.inf'_eq_csInf_image theorem

(s : Finset ι) (H : s.Nonempty) (f : ι → α) : s.inf' H f = sInf (f '' s)

Full source

theorem inf'_eq_csInf_image (s : Finset ι) (H : s.Nonempty) (f : ι → α) :
    s.inf' H f = sInf (f '' s) :=
  sup'_eq_csSup_image (α := αᵒᵈ) _ H _

Equality of Finite Infimum and Image Infimum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, $s$ a nonempty finite set of type $\iota$, and $f : \iota \to \alpha$ a function. Then the infimum of $f$ over $s$ (denoted $s.\text{inf}'\, H\, f$) is equal to the infimum of the image of $f$ over $s$ (denoted $\inf (f \,''\, s)$). In other words: \[ \inf_{i \in s} f(i) = \inf \{ f(i) \mid i \in s \}. \]

Finset.sup'_id_eq_csSup theorem

(s : Finset α) (hs) : s.sup' hs id = sSup s

Full source

theorem sup'_id_eq_csSup (s : Finset α) (hs) : s.sup' hs id = sSup s := by
  rw [sup'_eq_csSup_image s hs, Set.image_id]

Finite Supremum Equals Lattice Supremum for Identity Function

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty finite subset of $\alpha$. Then the supremum of $s$ computed via `Finset.sup'` with the identity function equals the supremum of $s$ in the lattice, i.e., \[ \sup'_{\text{Fin}} s = \sup s. \]

Finset.inf'_id_eq_csInf theorem

(s : Finset α) (hs) : s.inf' hs id = sInf s

Full source

theorem inf'_id_eq_csInf (s : Finset α) (hs) : s.inf' hs id = sInf s :=
  sup'_id_eq_csSup (α := αᵒᵈ) _ hs

Finite Infimum Equals Lattice Infimum for Identity Function

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty finite subset of $\alpha$. Then the infimum of $s$ computed via `Finset.inf'` with the identity function equals the infimum of $s$ in the lattice, i.e., \[ \inf'_{\text{Fin}} s = \inf s. \]

Finset.sup'_univ_eq_ciSup theorem

(f : ι → α) : univ.sup' univ_nonempty f = ⨆ i, f i

Full source

lemma sup'_univ_eq_ciSup (f : ι → α) : univ.sup' univ_nonempty f = ⨆ i, f i := by
  simp [sup'_eq_csSup_image, iSup]

Equality of Finite Supremum and Indexed Supremum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $\iota$ be a finite type. For any function $f : \iota \to \alpha$, the supremum of $f$ over the universal finset (which is nonempty since $\iota$ is finite) equals the indexed supremum of $f$ over all elements of $\iota$, i.e., $$\sup_{i \in \text{univ}} f(i) = \bigsqcup_{i \in \iota} f(i).$$

Finset.inf'_univ_eq_ciInf theorem

(f : ι → α) : univ.inf' univ_nonempty f = ⨅ i, f i

Full source

lemma inf'_univ_eq_ciInf (f : ι → α) : univ.inf' univ_nonempty f = ⨅ i, f i := by
  simp [inf'_eq_csInf_image, iInf]

Equality of Finite Infimum and Indexed Infimum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $\iota$ a finite type. For any function $f : \iota \to \alpha$, the infimum of $f$ over the universal finset (which is nonempty since $\iota$ is finite) equals the indexed infimum of $f$ over all elements of $\iota$, i.e., $$\inf_{i \in \text{univ}} f(i) = \bigsqcap_{i \in \iota} f(i).$$

Finset.sup_univ_eq_ciSup theorem

[Fintype ι] (f : ι → α) : univ.sup f = ⨆ i, f i

Full source

lemma sup_univ_eq_ciSup [Fintype ι] (f : ι → α) : univ.sup f = ⨆ i, f i :=
  le_antisymm
    (Finset.sup_le fun _ _ => le_ciSup (finite_range _).bddAbove _)
    (ciSup_le' fun _ => Finset.le_sup (mem_univ _))

Supremum over Universal Finset Equals Indexed Supremum for Finite Types

Informal description

For a finite type $\iota$ and a function $f : \iota \to \alpha$ where $\alpha$ is a conditionally complete lattice, the supremum of $f$ over the universal finset (containing all elements of $\iota$) equals the indexed supremum of $f$, i.e., $$\sup_{i \in \text{univ}} f(i) = \bigsqcup_{i} f(i).$$

Finset.Nonempty.ciSup_mem_image theorem

{s : Finset ι} (h : s.Nonempty) : ⨆ i ∈ s, f i ∈ s.image f

Full source

theorem Finset.Nonempty.ciSup_mem_image {s : Finset ι} (h : s.Nonempty) :
    ⨆ i ∈ s, f i⨆ i ∈ s, f i ∈ s.image f :=
  s.ciSup_mem_image _ (h.imp (by simp))

Supremum of Function over Nonempty Finite Set Belongs to Its Image

Informal description

Let $s$ be a nonempty finite set of elements of type $\iota$, and let $f : \iota \to \alpha$ be a function. Then the supremum of $f$ over $s$ is an element of the image of $s$ under $f$, i.e., $$\bigsqcup_{i \in s} f(i) \in f(s).$$

Set.Nonempty.ciSup_mem_image theorem

{s : Set ι} (h : s.Nonempty) (hs : s.Finite) : ⨆ i ∈ s, f i ∈ f '' s

Full source

theorem Set.Nonempty.ciSup_mem_image {s : Set ι} (h : s.Nonempty) (hs : s.Finite) :
    ⨆ i ∈ s, f i⨆ i ∈ s, f i ∈ f '' s :=
  hs.ciSup_mem_image _ (h.imp (by simp))

Supremum of Function over Nonempty Finite Set Belongs to Its Image

Informal description

For any nonempty finite set $s$ of elements of type $\iota$ and any function $f : \iota \to \alpha$ where $\alpha$ is a conditionally complete linear order, the supremum of $f$ over $s$ belongs to the image of $s$ under $f$, i.e., $$\bigsqcup_{i \in s} f(i) \in f(s).$$

Set.Nonempty.ciSup_lt_iff theorem

{s : Set ι} {a : α} {f : ι → α} (h : s.Nonempty) (hs : s.Finite) : ⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a

Full source

theorem Set.Nonempty.ciSup_lt_iff {s : Set ι} {a : α} {f : ι → α} (h : s.Nonempty) (hs : s.Finite) :
    ⨆ i ∈ s, f i⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a :=
  hs.ciSup_lt_iff (h.imp (by simp))

Supremum over Nonempty Finite Set is Less Than iff All Elements Are Less Than

Informal description

Let $s$ be a nonempty finite subset of a type $\iota$, and let $f : \iota \to \alpha$ be a function where $\alpha$ is a conditionally complete linear order. Then the supremum of $f$ over $s$ is less than a value $a$ if and only if $f(x) < a$ for all $x \in s$. In other words: \[ \sup_{i \in s} f(i) < a \leftrightarrow \forall x \in s, f(x) < a. \]

List.iSup_mem_map_of_ne_nil theorem

{l : List ι} (f : ι → α) (h : l ≠ []) : ⨆ x ∈ l, f x ∈ l.map f

Full source

lemma List.iSup_mem_map_of_ne_nil {l : List ι} (f : ι → α) (h : l ≠ []) :
    ⨆ x ∈ l, f x⨆ x ∈ l, f x ∈ l.map f :=
  l.iSup_mem_map_of_exists_sSup_empty_le _ (by simpa using exists_mem_of_ne_nil _ h)

Supremum of Function over Non-Empty List Belongs to Its Image

Informal description

Let $l$ be a non-empty list of elements of type $\iota$, and let $f : \iota \to \alpha$ be a function where $\alpha$ is a conditionally complete linear order. Then the supremum of $f$ over the list $l$ is an element of the image of $l$ under $f$, i.e., $\bigsqcup_{x \in l} f(x) \in f(l)$.

Multiset.iSup_mem_map_of_ne_zero theorem

{s : Multiset ι} (f : ι → α) (h : s ≠ 0) : ⨆ x ∈ s, f x ∈ s.map f

Full source

lemma Multiset.iSup_mem_map_of_ne_zero {s : Multiset ι} (f : ι → α) (h : s ≠ 0) :
    ⨆ x ∈ s, f x⨆ x ∈ s, f x ∈ s.map f :=
  s.iSup_mem_map_of_exists_sSup_empty_le _ (by simpa using exists_mem_of_ne_zero h)

Supremum of Function over Nonempty Multiset Belongs to Its Image

Informal description

Let $s$ be a nonempty multiset of elements of type $\iota$ in a conditionally complete linear order $\alpha$, and let $f : \iota \to \alpha$ be a function. Then the supremum of $f$ over all elements in $s$ belongs to the image of $s$ under $f$, i.e., $\bigsqcup_{x \in s} f(x) \in f(s)$.