ext_iff — Mathlib

English

Let L' be a Lie subalgebra of L. For x, y in L', we have x = y if and only if their ambient images in L are equal: (x : L) = (y : L).

Русский

Пусть L' ⊆ L является подалгеброй Л. Для любых x, y ∈ L' верно: x = y тогда и только если их образы в L совпадают: (x : L) = (y : L).

LaTeX

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

Lean4

theorem ext_iff (x y : L') : x = y ↔ (x : L) = y :=
  Subtype.ext_iff

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