coe_mk' — Mathlib

English

An explicit constructor assembling an affine equivalence from a base map, a linear part, a base point and a compatibility condition.

Русский

Явное конструкторское определение, собирающее аффинное эквивалентное отображение из базового отображения, линейной части, базовой точки и условия совместимости.

LaTeX

$$$\mathrm{mk'}(e,e',p,h) \in P_1 \overset{\text{Affine}}{\to} P_2$$$

Lean4

@[simp]
theorem coe_mk' (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p h) : ⇑(mk' e e' p h) = e :=
  rfl

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