toIsometryEquiv_refl — Mathlib

English

The isometry equivalence corresponding to a reflexive isomorphism is the reflexive isometry.

Русский

Изометрическое эквивалентное отображение, связанное с тождественным изоморфизмом, есть тождественная изометрия.

LaTeX

$$$\\text{toIsometryEquiv}(\\mathrm{refl}\\ X) = \\mathrm{refl} (X.\\mathrm{form})$$$

Lean4

@[simp]
theorem toIsometryEquiv_refl : toIsometryEquiv (.refl X) = .refl _ :=
  rfl

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