inverse_domain — Mathlib

English

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

Русский

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

LaTeX

$$(\\mathrm{domain}(f^{-1})) = \\mathrm{range}(f.toFun)$$

Lean4

theorem inverse_domain : (inverse f).domain = LinearMap.range f.toFun :=
  by
  rw [inverse, Submodule.toLinearPMap_domain, ← graph_map_snd_eq_range, ← LinearEquiv.fst_comp_prodComm,
    Submodule.map_comp]
  rfl

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