prod_mono

Mathlib.Algebra.Star.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalStarSubalgebra.prod_mono

← MathLib Explorer

English

If S ≤ T and S1 ≤ T1 then S × S1 ≤ T × T1.

Русский

Если S ≤ T и S1 ≤ T1, то произведение S × S1 вложено в T × T1.

LaTeX

$$$S \\le T \\;\\land\\; S_1 \\le T_1 \\Rightarrow S.prod S_1 \\le T.prod T_1$$$

Lean4

theorem prod_mono {S T : NonUnitalStarSubalgebra R A} {S₁ T₁ : NonUnitalStarSubalgebra R B} :
    S ≤ T → S₁ ≤ T₁ → prod S S₁ ≤ prod T T₁ :=
  Set.prod_mono

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru