ofLe — Mathlib

English

Definition: If K ≤ K', then K viewed as a Lie subalgebra of K' is given by the range of the inclusion map.

Русский

Определение: если K ≤ K', то K рассматривается как подалгебра внутри K' и описывается как образ включения.

LaTeX

$$def ofLe : LieSubalgebra R K' := (inclusion h).range$$

Lean4

/-- Given two nested Lie subalgebras `K ⊆ K'`, we can view `K` as a Lie subalgebra of `K'`,
regarded as Lie algebra in its own right. -/
def ofLe : LieSubalgebra R K' :=
  (inclusion h).range

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