prod_mono

Mathlib.Algebra.Algebra.Subalgebra.Prod

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

English

If S ≤ T in A and S₁ ≤ T₁ in B, then S × S₁ ≤ T × T₁.

Русский

Если S ≤ T в A и S₁ ≤ T₁ в B, то S × S₁ ≤ T × T₁.

LaTeX

$$prod_mono : S ≤ T → S₁ ≤ T₁ → prod S S₁ ≤ prod T T₁$$

Lean4

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

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

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

Разделы

Аффилиация

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