coe_comp_to_continuous_fun — Mathlib

English

For f ∈ C_c(γ, δ) and g ∈ β →co γ, the function (f.comp g) viewed as a function β → δ equals the composition f ∘ g.

Русский

Для f ∈ C_c(γ, δ) и g ∈ β →co γ функция (f.comp g), рассматриваемая как функция β → δ, равна композиции f ∘ g.

LaTeX

$$$$ ((f.comp g) : β \to δ) = f \circ g. $$$$

Lean4

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

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