English
A submodule equals the supremum of the spans of its nonzero elements: p = sSup { T | ∃ m ∈ p, m ≠ 0 ∧ T = span{m} }.
Русский
Подмодуль равен наибольшему верхнему пределу оболочек его ненулевых элементов: p = sup { span{m} : m ∈ p, m ≠ 0 }.
LaTeX
$$p = sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = span_R{ m }}$$
Lean4
/-- A submodule is equal to the supremum of the spans of the submodule's nonzero elements. -/
theorem submodule_eq_sSup_le_nonzero_spans (p : Submodule R M) :
p = sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = span R { m }} :=
by
let S := {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = span R { m }}
apply le_antisymm
· intro m hm
by_cases h : m = 0
· rw [h]
simp
· exact @le_sSup _ _ S _ ⟨m, ⟨hm, ⟨h, rfl⟩⟩⟩ m (mem_span_singleton_self m)
· rw [sSup_le_iff]
rintro S ⟨_, ⟨_, ⟨_, rfl⟩⟩⟩
rwa [span_singleton_le_iff_mem]
