mk_div — Mathlib

English

For measurable f,g with AEStronglyMeasurable representatives hf,hg, the construction commutes with division: mk(f/g) equals mk(f)/mk(g) under the corresponding measurability assumptions.

Русский

Для измеримых f,g с представителями AEStronglyMeasurable hf,hg, конструирование деления сохраняется: mk(f/g) равно mk(f)/mk(g) при соответствующих предпосылках измеримости.

LaTeX

$$$\text{mk}(f/g)\,(hf.div hg) = (\text{mk}~f~hf) / (\text{mk}~g~hg).$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_div (f g : α → γ) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
    mk (f / g) (hf.div hg) = (mk f hf : α →ₘ[μ] γ) / mk g hg :=
  rfl

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