English
Let X be a space and Y be a type with a division operation. For any locally constant functions f, g : X → Y, the quotient f / g is obtained pointwise, i.e. (f / g)(x) = f(x) / g(x) for all x ∈ X. In particular, the underlying function of f / g coincides with the pointwise division of their values.
Русский
Пусть X — топологическое пространство, Y — множество с операцией деления. Для любых локально константных отображений f, g: X → Y рецепт деления определяется по точкам: (f / g)(x) = f(x) / g(x) для всех x ∈ X. Следовательно, функция, соответствующая f / g, совпадает с точечной операцией деления.
LaTeX
$$$(f/g) = \lambda x.\; f(x)/g(x).$$$
Lean4
@[to_additive]
theorem coe_div [Div Y] (f g : LocallyConstant X Y) : ⇑(f / g) = f / g :=
rfl
