coe_toAffineMap — Mathlib

English

Given f: P →ᵃ[R] Q, and h is a proof that the map is affine, the structure built from ⟨f,h⟩ has toAffineMap component f.

Русский

Если дано f: P →ᵃ[R] Q и доказано, что отображение аффинно, то структура ⟨f,h⟩ имеет toAffineMap-компоненту равную f.

LaTeX

$$$(f : P \toᵃ[R] Q) (h) : ((⟨f, h⟩ : P →ᴬ[R] Q) : P →ᵃ[R] Q) = f$$$

Lean4

@[simp, norm_cast]
theorem coe_toAffineMap (f : P →ᴬ[R] Q) : ((f : P →ᵃ[R] Q) : P → Q) = f :=
  rfl

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