linearIsometryEquiv_mk' — Mathlib

English

Given e, e', p, h, the construction mk'(e,e',p,h) yields an affine isometry equivalence whose linear part is e'.

Русский

Пусть заданы e, e', p, h; конструирование mk'(e,e',p,h) даёт аффинную изометрическую эквивалентность с линейной частью e'.

LaTeX

$$$$ (mk'\, e\, e'\, p\, h).linearIsometryEquiv = e'. $$$$

Lean4

@[simp]
theorem linearIsometryEquiv_mk' (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p h) : (mk' e e' p h).linearIsometryEquiv = e' :=
  by
  ext
  rfl

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