div_comp — Mathlib

English

If f and g are continuous with γ a topological space, then (f/g).comp h = (f.comp h) / (g.comp h).

Русский

Пусть f,g непрерывны, γ — топологическое пространство; тогда (f/g)∘h = (f∘h)/(g∘h).

LaTeX

$$$\forall f,g:\ C(\beta,\gamma),\ \forall h:\ C(\alpha,\beta): (f/g)\circ h = (f\circ h)/(g\circ h).$$$

Lean4

@[to_additive (attr := simp)]
theorem div_comp [Div γ] [ContinuousDiv γ] (f g : C(β, γ)) (h : C(α, β)) : (f / g).comp h = f.comp h / g.comp h :=
  rfl

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