coe_comp — Mathlib

English

The underlying function of the composition equals the composition of underlying functions.

Русский

Базовая функция композиции удовлетворяет равенству $\\mathrm{coe}(f \\circ g) = \\mathrm{coe}(f) \\circ \\mathrm{coe}(g)$.

LaTeX

$$$\\text{coe}(f\\circ g) = \\mathrm{coe}(f) \\circ \\mathrm{coe}(g)$$$

Lean4

/-- Composition of affine maps acts as applying the two functions. -/
@[simp]
theorem coe_comp (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) : ⇑(f.comp g) = f ∘ g :=
  rfl

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