surjective_π_iff_span_eq_top — Mathlib

English

π is surjective if and only if the span of the solution variables equals the top submodule.

Русский

π сюрьективен тогда и только тогда, когда оболочка переменных решения равна верхнему подмодулю.

LaTeX

$$$\text{Surjective}(\text{solution.π}) \; \iff \; \operatorname{span}_A(\mathrm{Set.range}(\text{solution.var})) = \top$$$

Lean4

theorem surjective_π_iff_span_eq_top : Function.Surjective solution.π ↔ Submodule.span A (Set.range solution.var) = ⊤ :=
  by rw [← LinearMap.range_eq_top, range_π]

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