map_equivMapOfInjective_symm_apply

English

If f is injective, the composition f ∘ (equivMapOfInjective f i p) equals the inclusion into M₂ by f.

Русский

Если f инъективно, то композиция f с эквивалентностью равна очевидному включению через f на p.map f.

LaTeX

$$$f ( (\\text{equivMapOfInjective } f\\; i\\; p)^{-1} x) = x$ for appropriate x$$

Lean4

@[simp]
theorem map_equivMapOfInjective_symm_apply (f : F) (i : Injective f) (p : Submodule R M) (x : p.map f) :
    f ((equivMapOfInjective f i p).symm x) = x := by
  rw [← LinearEquiv.apply_symm_apply (equivMapOfInjective f i p) x, coe_equivMapOfInjective_apply, i.eq_iff,
    LinearEquiv.apply_symm_apply]

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