coe_ofSurjective — Mathlib

English

The inverse evaluation aligns with the inverse linear map under surjective construction.

Русский

Оценка обратного отображения совпадает с обратной линейной картой при конструировании по сюръективности.

LaTeX

$$coe_ofSurjective_symm_2 : ((LinearIsometryEquiv.ofSurjective f hfr).symm) = (g)$$

Lean4

@[simp]
theorem coe_ofSurjective (f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : Function.Surjective f) :
    ⇑(LinearIsometryEquiv.ofSurjective f hfr) = f := by
  ext
  rfl

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