English
For a Submodule p ⊆ M, the equality (lieSpan_R L (p:Set M) : Submodule R M) = p holds exactly when there exists a LieSubmodule N with ↑N = p.
Русский
Для подмодуля p выполняется равенство (lieSpan_R L (p:Set M): Submodule R M) = p тогда, когда существует LieSubmodule N such that ↑N = p.
LaTeX
$$(\\operatorname{lieSpan}_{R,L}(p:\\text{Set} M) : \\text{Submodule } R M) = p \\;\\iff\\; \\exists N : \\text{LieSubmodule } R L M, \\uparrow N = p$$
Lean4
theorem coe_lieSpan_submodule_eq_iff {p : Submodule R M} :
(lieSpan R L (p : Set M) : Submodule R M) = p ↔ ∃ N : LieSubmodule R L M, ↑N = p :=
by
rw [p.exists_lieSubmodule_coe_eq_iff L]; constructor <;> intro h
· intro x m hm; rw [← h, mem_toSubmodule]; exact lie_mem _ (subset_lieSpan hm)
· rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_eq]
