span_singleton_eq_top_iff — Mathlib

English

For submodules p, p', p ⊔ p' = ⊤ iff for every m ∈ M there exist u ∈ p and v ∈ p' with m = u + v.

Русский

p ⊔ p' = ⊤ тогда и только тогда, когда для каждого m ∈ M найдутся u ∈ p и v ∈ p' такие, что m = u + v.

LaTeX

$$$$ p \\sqcup p' = \\top \\iff \\forall m \\in M, \\exists u \\in p, \\exists v \\in p', m = u + v. $$$$

Lean4

theorem span_singleton_eq_top_iff (x : M) : (R ∙ x) = ⊤ ↔ ∀ v, ∃ r : R, r • x = v :=
  by
  rw [eq_top_iff, le_span_singleton_iff]
  tauto

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