coe_toRealLinearIsometryEquivOfMapZero

English

For any isometry f: E ≃ᵢ F and h0: f 0 = 0, the real linear isometry equivalence f.toRealLinearIsometryEquivOfMapZero h0 equals f.

Русский

Для изометрии f: E ≃ᵢ F и условия h0: f 0 = 0, получаемое отображение f.toRealLinearIsometryEquivOfMapZero совпадает с f.

LaTeX

$$$f^{\text{toRealLinearIsometryEquivOfMapZero}}(h0) = f$$$

Lean4

@[simp]
theorem coe_toRealLinearIsometryEquivOfMapZero (f : E ≃ᵢ F) (h0 : f 0 = 0) :
    ⇑(f.toRealLinearIsometryEquivOfMapZero h0) = f :=
  rfl

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