sub — Mathlib

English

The supremum of two Finite Strongly Measurable functions is Finite Strongly Measurable.

Русский

Супремум двух финитно сильнос измеримых функций — финитно сильно измерим.

LaTeX

$$$\text{FinStronglyMeasurable}(f) \land \text{FinStronglyMeasurable}(g) \Rightarrow \text{FinStronglyMeasurable}(f \sqcup g)$$$

Lean4

@[measurability]
protected theorem sub [SubtractionMonoid β] [ContinuousSub β] (hf : FinStronglyMeasurable f μ)
    (hg : FinStronglyMeasurable g μ) : FinStronglyMeasurable (f - g) μ :=
  ⟨fun n => hf.approx n - hg.approx n, fun n =>
    (measure_mono (Function.support_sub _ _)).trans_lt
      ((measure_union_le _ _).trans_lt (ENNReal.add_lt_top.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩)),
    fun x => (hf.tendsto_approx x).sub (hg.tendsto_approx x)⟩

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