coe_mk — Mathlib

English

If e is an affine isometry between P and P2, and its linear part preserves norms, then the constructed map mk e equals e.

Русский

Если e — афинная изометрия между P и P2, и линейная часть сохраняет нормы, то полученная карта mk e совпадает с e.

LaTeX

$$$\\text{If } e : P \\simeq^a[\\mathbb{K}] P_2 \\text{ and } \\forall x, \\|e.linear x\\| = \\|x\\|, \\; \\text{then } \\mathrm{toFun}(\\mathrm{mk}(e, \\cdot)) = e$$$

Lean4

@[simp]
theorem coe_mk (e : P ≃ᵃ[𝕜] P₂) (he : ∀ x, ‖e.linear x‖ = ‖x‖) : ⇑(mk e he) = e :=
  rfl

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