sup_toSubalgebra_of_left — Mathlib

English

If E1 is finite-dimensional over K, then the subalgebra of the join equals the join of the subalgebras: (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra.

Русский

Если E1 конечномерно над K, то подалгебра объединения равна объединению подалгебр.

LaTeX

$$$[\text{FD}]\ (E_1)\toSubalgebra = E_1^{\toSubalgebra} \lor E_2^{\toSubalgebra}$$$

Lean4

theorem sup_toSubalgebra_of_left [FiniteDimensional K E1] :
    (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra :=
  sup_toSubalgebra_of_isAlgebraic_left E1 E2

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