iSup_monotone' — Mathlib

English

A one-variable version: for f: Nat→α→ENNReal, iSup_monotone' asserts monotonicity in the index for a fixed x.

Русский

Одномерная версия: для f: Nat→α→ENNReal, утверждается монотонность по индексу для фиксированного x.

LaTeX

$$$$ \\text{Monotone } n \\mapsto a \\mapsto \\big\\lceil \\big\\vee_{k≤n} f_k(a) \\big\\rceil $$$$

Lean4

theorem iSup_monotone' {α : Type*} (f : ℕ → α → ℝ≥0∞) (x : α) : Monotone fun n ↦ ⨆ (k) (_ : k ≤ n), f k x :=
  fun _ _ hnm ↦ iSup_monotone f hnm x

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