instMeasurableMul₂ — Mathlib

English

Multiplication on EReal is a measurable operation in two arguments.

Русский

Умножение на EReal измеримо как операция из двух аргументов.

LaTeX

$$$\\operatorname{MeasurableMul_2}\\; \\mathrm{EReal}$$$

Lean4

instance : MeasurableMul₂ EReal := by
  refine ⟨measurable_of_real_real ?_ ?_ ?_ ?_ ?_⟩
  · exact (measurable_fst.mul measurable_snd).coe_real_ereal
  · exact (measurable_const_mul _).comp measurable_coe_real_ereal
  · exact (measurable_const_mul _).comp measurable_coe_real_ereal
  · simp_rw [mul_comm _ ⊥]
    exact (measurable_const_mul _).comp measurable_coe_real_ereal
  · simp_rw [mul_comm _ ⊤]
    exact (measurable_const_mul _).comp measurable_coe_real_ereal

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