ext_iff' — Mathlib

English

Two Lie subalgebras L₁', L₂' of L are equal if and only if they have exactly the same elements; i.e., x ∈ L₁' ⇔ x ∈ L₂' for all x ∈ L.

Русский

Две подалгебры L₁', L₂' под L равны тогда, когда для каждого x ∈ L выполнено x ∈ L₁' ⇔ x ∈ 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),\ L' = L'' \iff \forall x, x \in L' \iff x \in L''.$$$$

Lean4

theorem ext_iff' (L₁' L₂' : LieSubalgebra R L) : L₁' = L₂' ↔ ∀ x, x ∈ L₁' ↔ x ∈ L₂' :=
  SetLike.ext_iff

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