instCanLiftSubmoduleToSubmoduleForallForallForallMemBracket

English

If a Submodule N of M is closed under all brackets [x, m] with x ∈ L and m ∈ N, then N inherits a LieSubmodule structure.

Русский

Если подмодуль N модуля M замкнут относительно всех скобок [x, m] с x ∈ L и m ∈ N, то N наследует структуру LieSubmodule.

LaTeX

$$If (∀ x ∈ L)(∀ m ∈ N), ⁅x,m⁆ ∈ N, then N is a LieSubmodule of M$$

Lean4

instance : CanLift (Submodule R M) (LieSubmodule R L M) (·) (fun N ↦ ∀ {x : L} {m : M}, m ∈ N → ⁅x, m⁆ ∈ N) where
  prf N hN := ⟨⟨N, hN⟩, rfl⟩

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