coe_div — Mathlib

English

The evaluation map commutes with division: for f,g ∈ C(α,β), the function (f/g) as a continuous map equals the map sending x to f(x)/g(x).

Русский

Оценочная карта сохраняет операцию деления: функция (f/g) как непрерывное отображение равна отображению x ↦ f(x)/g(x).

LaTeX

$$$\forall f,g:\ C(\alpha,\beta): \operatorname{coe}(f/g) = \operatorname{coe}(f)/\operatorname{coe}(g).$$$

Lean4

@[to_additive (attr := norm_cast, simp)]
theorem coe_div [Div β] [ContinuousDiv β] (f g : C(α, β)) : ⇑(f / g) = f / g :=
  rfl

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