le_def — Mathlib

English

The partial order on LieSubalgebras is given by set inclusion of their underlying sets.

Русский

Частичный порядок подалгебр задаётся включением их носителей как множеств.

LaTeX

$$$$\forall {R} {L} [\text{CommRing } R] [\text{LieRing } L] [\text{LieAlgebra } R L]\ (K K' : \text{LieSubalgebra } R L),\ K \le K' \iff (K : \text{Set } L) \subseteq K'. $$$$

Lean4

theorem le_def : K ≤ K' ↔ (K : Set L) ⊆ K' :=
  Iff.rfl

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