coeFn_div — Mathlib

English

The pointwise division f/g of AEEqFun corresponds to almost everywhere equality of their function representations: the coerced function satisfies equality almost everywhere to the pointwise quotient.

Русский

Пусть f,g — AEEqFun. Чтобы f/g соответствовал точечному отношению, как функция: выводится равенство почти наверняка между полученной функцией и их делением в обычном смысле.

LaTeX

$$$\uparrow(f/g) =_{\mu} f/g$$$

Lean4

@[to_additive]
theorem coeFn_div (f g : α →ₘ[μ] γ) : ⇑(f / g) =ᵐ[μ] f / g :=
  coeFn_comp₂ _ _ _ _

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