iSup_comp_eq — Mathlib

English

Let f: β → α be monotone and s: ι → β with a cofinality condition: for every x, there exists i with x ≤ s(i). Then the iSup of f(s(i)) equals the iSup over all y of f(y): ⨆ x f(s(x)) = ⨆ y f(y).

Русский

Пусть f: β → α монотонна, и s: ι → β удовлетворяет кф-условию: для каждого x существует i, такое что x ≤ s(i). Тогда iSup f(s(i)) равно iSup f(y) по всем y.

LaTeX

$$$\\\\sup_{x} f(s(x)) = \\\\sup_{y} f(y)$$$

Lean4

theorem iSup_comp_eq [Preorder β] {f : β → α} (hf : Monotone f) {s : ι → β} (hs : ∀ x, ∃ i, x ≤ s i) :
    ⨆ x, f (s x) = ⨆ y, f y :=
  le_antisymm (iSup_comp_le _ _) (iSup_mono' fun x => (hs x).imp fun _ hi => hf hi)

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