range_restrictDom — Mathlib

English

The range of restrictDom is the whole module, i.e., surjective onto the ambient submodule.

Русский

Область значений restrictDom равна всему модулю; отображение сюръективно на исходный модуль.

LaTeX

$$$\mathrm{range}(\mathrm{restrictDom}(M,R,s)) = \top$$$

Lean4

theorem range_restrictDom (s : Set α) [DecidablePred (· ∈ s)] : LinearMap.range (restrictDom M R s) = ⊤ :=
  range_eq_top.2 <| Function.RightInverse.surjective <| LinearMap.congr_fun (restrictDom_comp_subtype s)

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