iInf_comp_eq — Mathlib

English

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

Русский

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

LaTeX

$$$\\\\inf_{i} f(s(i)) = \\\\inf_{y} f(y)$$$

Lean4

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

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