iSup_mono' — Mathlib

English

Let α be a complete lattice and f : ι → α, g : ι' → α with the property that for every i there exists i' such that f(i) ≤ g(i'). Then iSup f ≤ iSup g.

Русский

Пусть α — полная решетка и имеются функции f: ι → α, g: ι' → α such that для каждого i существует i' с f(i) ≤ g(i'). Тогда iSup f ≤ iSup g.

LaTeX

$$$\\\\forall f : ι \\\\to α, g : ι' \\\\to α, \\\\left( \\\\forall i, \\\\exists i', f(i) \\\\le g(i') \\\\right) \\\\Rightarrow iSup f \\\\le iSup g$$$

Lean4

theorem iSup_mono' {g : ι' → α} (h : ∀ i, ∃ i', f i ≤ g i') : iSup f ≤ iSup g :=
  iSup_le fun i => Exists.elim (h i) le_iSup_of_le

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