equivRange_symm_toLinearEquiv — Mathlib

English

The coercion from the equivalence range to the linear map range coincides with the rangeRestrict.

Русский

Переобразование из эквивалентности в диапазон линейного отображения совпадает с rangeRestrict.

LaTeX

$$$f.equivRange \\;hinj\\;hclo = f.rangeRestrict$$$

Lean4

@[simp]
theorem equivRange_symm_toLinearEquiv (hinj : Injective f) (hclo : IsClosed (range f)) :
    (f.equivRange hinj hclo).toLinearEquiv.symm = (LinearEquiv.ofInjective f.toLinearMap hinj).symm :=
  rfl

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