instDivOfContinuousDiv — Mathlib

English

If β has a continuous division, then for f,g ∈ C(α,β) the quotient (f/g)(x) = f(x)/g(x) is continuous, and (f/g) ∈ C(α,β).

Русский

Если β имеет непрерывное деление, то для любых f,g ∈ C(α,β) частное (f/g)(x) = f(x)/g(x) непрерывно, и (f/g) ∈ C(α,β).

LaTeX

$$$\forall f,g:\ C(\alpha,\beta): (f/g)(x) = f(x)/g(x) \quad\text{for all } x \in \alpha,$ and (f/g) ∈ C(\alpha,\beta).$$

Lean4

@[to_additive]
instance [Div β] [ContinuousDiv β] : Div C(α, β) where div f g := ⟨f / g, f.continuous.div' g.continuous⟩

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