exists_lieIdeal_coe_eq_iff — Mathlib

English

There exists a LieIdeal I with I mapped to K as LieSubalgebra, iff K is closed under brackets with all elements of the ambient Lie algebra.

Русский

Существует LieIdeal I, который отображается в K как LieSubalgebra, тогда как K замкнута относительно скобки со всеми элементами лежащими в L.

LaTeX

$$$\exists I \; (\uparrow I = K) \; \Leftrightarrow \forall x,y \in L, y \in K \rightarrow [x,y] \in K$$$

Lean4

theorem exists_lieIdeal_coe_eq_iff : (∃ I : LieIdeal R L, ↑I = K) ↔ ∀ x y : L, y ∈ K → ⁅x, y⁆ ∈ K := by
  simp only [← toSubmodule_inj, LieIdeal.toLieSubalgebra_toSubmodule, Submodule.exists_lieSubmodule_coe_eq_iff L,
    mem_toSubmodule]

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