partialSups_mono — Mathlib

English

partialSups is monotone: if f ≤ g then partialSups f ≤ partialSups g.

Русский

partialSups монотонна по отношению к входной функции: f ≤ g ⇒ partialSups f ≤ partialSups g.

LaTeX

$$$f \\le g \\Rightarrow \\mathrm{partialSups}\\, f \\le \\mathrm{partialSups}\\, g$$$

Lean4

theorem partialSups_mono : Monotone (partialSups : (ι → α) → ι →o α) := fun _ _ h _ ↦
  partialSups_le_iff.2 fun j hj ↦ (h j).trans (le_partialSups_of_le _ hj)

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