range_domRestrict_le_range — Mathlib

English

If f is surjective on the relevant scalars, then the range of the restricted map is contained in the range of f: range(f.domRestrict S) ≤ range f.

Русский

При условии сюръективности соответствующих скаляров образ ограниченного отображения содержится в диапазоне исходного отображения: range(f.domRestrict S) ≤ range f.

LaTeX

$$$\operatorname{range}(f.\mathrm{domRestrict} S) \le \operatorname{range} f$$$

Lean4

theorem range_domRestrict_le_range [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (S : Submodule R M) :
    LinearMap.range (f.domRestrict S) ≤ LinearMap.range f :=
  by
  rintro x ⟨⟨y, hy⟩, rfl⟩
  exact LinearMap.mem_range_self f y

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