coe_comp_to_continuous_fun — Mathlib

English

The underlying function of the composed map equals the composition of the underlying functions: (f.comp g) as a function equals f ∘ g.

Русский

Базовая функция композиции совпадает с композицией базовых функций: (f.comp g) как функция равна f ∘ g.

LaTeX

$$$((f.comp\; g) : \beta \to \delta) = f \circ g$$$

Lean4

@[simp]
theorem coe_comp_to_continuous_fun (f : C₀(γ, δ)) (g : β →co γ) : ((f.comp g) : β → δ) = f ∘ g :=
  rfl

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