English
For injective f with closed range, the inverse of the equivalence maps back appropriately: (f.equivRange hinj hclo)^{-1}(f(x)) = x.
Русский
Для инъективного отображения с замкнутым диапазоном обратное отображение эквивалентности восстанавливает исходный элемент: (f.equivRange hinj hclo)^{-1}(f(x)) = x.
LaTeX
$$$\\bigl(f.\\mathrm{equivRange}(hinj,hclo)\\bigr)^{-1}(f(x)) = x$$$
Lean4
@[simp]
theorem equivRange_symm_apply (hinj : Injective f) (hclo : IsClosed (range f)) (x : E) :
(f.equivRange hinj hclo).symm ⟨f x, by simp⟩ = x :=
by
suffices f ((f.equivRange hinj hclo).symm ⟨f x, by simp⟩) = f x from hinj this
trans f ((f.equivRange hinj hclo).symm.toLinearEquiv ⟨f x, by simp⟩)
·
rfl -- is there an API lemma for this already?
simp only [ContinuousLinearEquiv.toLinearEquiv_symm, equivRange_symm_toLinearEquiv]
set x' : LinearMap.range f := ⟨f x, by simp⟩
set f' : E →ₛₗ[σ] F := ↑f
change f' ((LinearEquiv.ofInjective f' hinj).symm x') = _
rw [LinearEquiv.ofInjective_symm_apply (f := f') (h := hinj) x']
