ciSup_mono' — Mathlib

English

If for every i there exists i' with f(i) ≤ g(i'), and g is bounded above, then iSup f ≤ iSup g.

Русский

Если для каждого i существует i' с f(i) ≤ g(i') и множество g ограничено сверху, то sup f ≤ sup g.

LaTeX

$$$ (\forall i, \exists i', f(i) \le g(i')) \rightarrow iSup f \le iSup g $$$

Lean4

theorem ciSup_mono' {ι'} {f : ι → α} {g : ι' → α} (hg : BddAbove (range g)) (h : ∀ i, ∃ i', f i ≤ g i') :
    iSup f ≤ iSup g :=
  ciSup_le' fun i => Exists.elim (h i) (le_ciSup_of_le hg)

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