coe_mk — Mathlib

English

When constructing an affine map from a function f, a linear part, and a compatibility proof, coercing this constructed map back to a function yields f.

Русский

При построении аффинного отображения из функции f, линейной части и подтверждения совместимости, возврат к функции даёт ту же самую f.

LaTeX

$$$((mk f\,\, linear\,\, add) : P_1 \to^a_k P_2)\,\;\!:\, P_1 \to P_2 = f$$$

Lean4

/-- Constructing an affine map and coercing back to a function
produces the same map. -/
@[simp]
theorem coe_mk (f : P1 → P2) (linear add) : ((mk f linear add : P1 →ᵃ[k] P2) : P1 → P2) = f :=
  rfl

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