lie_le_iff — Mathlib

English

The bracket [I,N] is contained in N' iff every bracket [x,m] with x ∈ I and m ∈ N lies in N'.

Русский

Скобка [I,N] содержится в N' тогда и только тогда, когда для всех x ∈ I и m ∈ N скобка [x,m] принадлежит N'.

LaTeX

$$$$ [I,N] \le N' \iff \forall x \in I, \forall m \in N, [x,m] \in N'. $$$$

Lean4

theorem lie_le_iff : ⁅I, N⁆ ≤ N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N' :=
  by
  rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]
  refine ⟨fun h x hx m hm => h ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩, ?_⟩
  rintro h _ ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩
  exact h x hx m hm

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