ext — Mathlib

English

If L₁' and L₂' are Lie subalgebras of L and every element of L is in L₁' precisely when it is in L₂', then L₁' = L₂'.

Русский

Если L₁' и L₂' — подалгебры L, и для каждого x в L выполняется x ∈ L₁' ⇔ x ∈ L₂', то L₁' = L₂'.

LaTeX

$$$$\forall {R : Type u} {L : Type v} [\text{CommRing } R] [\text{LieRing } L] [\text{LieAlgebra } R L] (L' L'' : \text{LieSubalgebra } R L),\ (\forall x, x \in L' \leftrightarrow x \in L'') \Rightarrow L' = L''. $$$$

Lean4

@[ext]
theorem ext (L₁' L₂' : LieSubalgebra R L) (h : ∀ x, x ∈ L₁' ↔ x ∈ L₂') : L₁' = L₂' :=
  SetLike.ext h

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