prod_mono

Mathlib.Algebra.Group.Subsemigroup.Operations

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

← MathLib Explorer

English

If S1 ≤ S2 in M and T1 ≤ T2 in N, then S1.prod T1 ≤ S2.prod T2 in M × N.

Русский

Если S1 ⊆ S2 в M и T1 ⊆ T2 в N, то S1.prod T1 ⊆ S2.prod T2 в M × N.

LaTeX

$$S1 ≤ S2 → T1 ≤ T2 → S1.prod T1 ≤ S2.prod T2$$

Lean4

@[to_additive prod_mono]
theorem prod_mono {s₁ s₂ : Subsemigroup M} {t₁ t₂ : Subsemigroup N} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :
    s₁.prod t₁ ≤ s₂.prod t₂ :=
  Set.prod_mono hs ht

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

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

Разделы

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

Аффилиация

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