span_eq_top_iff_finite — Mathlib

English

A span equals the whole ring if and only if there exists a finite generating subset whose span is top.

Русский

Порождение всего кольца равно всему кольцу тогда и только тогда, когда существует конечное порождающее подмножество, дающее верхний результат.

LaTeX

$$$$ \operatorname{span}(s) = \top \iff \exists s' : \mathrm{Finset}(\alpha), \uparrow s' \subseteq s \land \operatorname{span}(s' : \mathrm{Set}(\alpha)) = \top $$$$

Lean4

theorem span_eq_top_iff_finite (s : Set α) : span s = ⊤ ↔ ∃ s' : Finset α, ↑s' ⊆ s ∧ span (s' : Set α) = ⊤ :=
  by
  simp_rw [eq_top_iff_one]
  exact ⟨Submodule.mem_span_finite_of_mem_span, fun ⟨s', h₁, h₂⟩ => span_mono h₁ h₂⟩

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