English
Let S be a subset of M and h1, h2, h3, h4 be the closure data used to form a Lie submodule from S. Then for every x ∈ M, x belongs to the constructed Lie submodule ⟨⟨⟨⟨S, h1⟩, h2⟩, h3⟩, h4⟩ if and only if x ∈ S.
Русский
Пусть S ⊆ M и даны данные замыкания h1, h2, h3, h4, используемые для образования подмодуля Ли из S. Тогда для каждого x ∈ M выполняется: x принадлежит полученному подмодулю Ли ⟨⟨⟨⟨S, h1⟩, h2⟩, h3⟩, h4⟩ тогда и только тогда, когда x ∈ S.
LaTeX
$$$ x \in \langle\langle\langle\langle S, h_1 \rangle, h_2 \rangle, h_3 \rangle, h_4 \rangle \;\iff\; x \in S $$$
Lean4
theorem mem_mk_iff (S : Set M) (h₁ h₂ h₃ h₄) {x : M} : x ∈ (⟨⟨⟨⟨S, h₁⟩, h₂⟩, h₃⟩, h₄⟩ : LieSubmodule R L M) ↔ x ∈ S :=
Iff.rfl
