inverse_range — Mathlib

English

The range of the inverse equals the domain of the original map.

Русский

Образ обратного равен области определения исходного отображения.

LaTeX

$$LinearMap.range (inverse f).toFun = f.domain$$

Lean4

theorem inverse_range : LinearMap.range (inverse f).toFun = f.domain :=
  by
  rw [inverse, Submodule.toLinearPMap_range _ (mem_inverse_graph_snd_eq_zero hf), ← graph_map_fst_eq_domain, ←
    LinearEquiv.snd_comp_prodComm, Submodule.map_comp]
  rfl

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