iSup_mem_measurableLE' — Mathlib

English

Analogous statement to iSup_mem_measurableLE but for ENNReal-valued functions in measurableLE.

Русский

Аналогично утверждению для ENNReal-значных функций в measurableLE.

LaTeX

$$$$ \\text{i.e. } (\\forall n, f_n \\in \\mathrm{measurableLE}(\\mu, \\nu)) \\Rightarrow (\\forall n, \\; \\text{the ENNReal valued supremum is in } \\mathrm{measurableLE}(\\mu, \\nu)). $$$$

Lean4

theorem iSup_mem_measurableLE' (f : ℕ → α → ℝ≥0∞) (hf : ∀ n, f n ∈ measurableLE μ ν) (n : ℕ) :
    (⨆ (k) (_ : k ≤ n), f k) ∈ measurableLE μ ν :=
  by
  convert iSup_mem_measurableLE f hf n
  simp

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