instMeasurableSub₂ — Mathlib

English

There is a MeasurableSub₂ structure on ENNReal, i.e., the two-variable sub operation is measurable.

Русский

Существует измеримая двувекторная операция вычитания ENNReal.

LaTeX

$$$\text{MeasurableSub₂ } ENNReal$$$

Lean4

instance instMeasurableSub₂ : MeasurableSub₂ ℝ≥0∞ :=
  ⟨by apply measurable_of_measurable_nnreal_nnreal <;> simp [tsub_eq_zero_of_le];
    exact continuous_sub.measurable.coe_nnreal_ennreal⟩

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