mem_mk_iff' — Mathlib

English

Let p be a submodule of M and h be a closure condition. Then for any x ∈ M, x ∈ (⟨p, h⟩) if and only if x ∈ p.

Русский

Пусть p — подпорядок M и дано условие замыкания h. Тогда для любого x ∈ M выполняется: x ∈ (⟨p, h⟩) тогда же, что и x ∈ p.

LaTeX

$$$ x \in (\langle p, h \rangle : LieSubmodule R L M) \;\iff\; x \in p $$$

Lean4

@[simp]
theorem mem_mk_iff' (p : Submodule R M) (h) {x : M} : x ∈ (⟨p, h⟩ : LieSubmodule R L M) ↔ x ∈ p :=
  Iff.rfl

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