le_sup_toSubalgebra — Mathlib

English

For intermediate fields E1 and E2 in a K-L extension, the generated subalgebras satisfy E1.toSubalgebra ⊔ E2.toSubalgebra ≤ (E1 ⊔ E2).toSubalgebra.

Русский

Для двух промежуточных полей E1 и E2 в расслоении K ⊆ L выполняется неравенство подалгебр, соответствующее их объединению.

LaTeX

$$$E_1^{\text{toSubalgebra}} \;\lor\; E_2^{\text{toSubalgebra}} \; \leq \; (E_1 \lor E_2)^{\text{toSubalgebra}}$$$

Lean4

theorem le_sup_toSubalgebra : E1.toSubalgebra ⊔ E2.toSubalgebra ≤ (E1 ⊔ E2).toSubalgebra :=
  sup_le (show E1 ≤ E1 ⊔ E2 from le_sup_left) (show E2 ≤ E1 ⊔ E2 from le_sup_right)

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