surjective_domRestrict_iff — Mathlib

English

For a semilinear map f, Surjective f.domRestrict S is equivalent to S ⊔ ker f = ⊤.

Русский

Для полупрямого отображения f, сюръективность f.domRestrict S эквивалентна S ⊔ ker f = ⊤.

LaTeX

$$$\operatorname{Surjective}(f.\mathrm{domRestrict} S) \iff S \;⊔\; \ker f = \top$$$

Lean4

@[simp]
theorem _root_.LinearMap.surjective_domRestrict_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} (hf : Surjective f) :
    Surjective (f.domRestrict S) ↔ S ⊔ LinearMap.ker f = ⊤ :=
  by
  rw [← LinearMap.range_eq_top] at hf ⊢
  rw [← hf]
  exact LinearMap.range_domRestrict_eq_range_iff

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