coe_toLinearEquiv — Mathlib

English

The function underlying a isometry equivalence coincides with its representation as a linear equivalence.

Русский

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

LaTeX

$$$\operatorname{coe\_toLinearEquiv}(f) = f$$$

Lean4

@[simp]
theorem coe_toLinearEquiv (f : Q₁.IsometryEquiv Q₂) : ⇑(f : M₁ ≃ₗ[R] M₂) = f :=
  rfl

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