ciSup_subtype'' — Mathlib

English

Let Nonempty ι and s ⊆ ι with s.Nonempty, and f : ι → α. Then the supremum over i ∈ s of f(i) equals the supremum over i : s of f(i) as i ranges over the elements of s.

Русский

Пусть непусто ι, s ⊆ ι непусто, и f: ι → α. Тогда sup по i∈s f(i) равен sup по i∈s (как элементам множества s).

LaTeX

$$$\sup_{i \in s} f(i) = \sup_{t \in s} f(t).$$$

Lean4

theorem ciSup_subtype'' {ι} [Nonempty ι] {s : Set ι} (hs : s.Nonempty) {f : ι → α}
    (hf : BddAbove (Set.range fun i : s ↦ f i)) (hf' : sSup ∅ ≤ ⨆ i : s, f i) :
    ⨆ i : s, f i = ⨆ (t : ι) (_ : t ∈ s), f t :=
  haveI : Nonempty s := Set.Nonempty.to_subtype hs
  ciSup_subtype hf hf'

Похожие утверждения