prod_mono_right

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Set.prod_mono_right

English

If t1 ⊆ t2 then s × t1 ⊆ s × t2.

Русский

Если t1 ⊆ t2, то s × t1 ⊆ s × t2.

LaTeX

$$$t_1 \\subseteq t_2 \\Rightarrow s \\times\\! t_1 \\subseteq s \\times\\! t_2$$$

Lean4

theorem prod_mono_right (ht : t₁ ⊆ t₂) : s ×ˢ t₁ ⊆ s ×ˢ t₂ :=
  prod_mono Subset.rfl ht

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

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

Разделы

Аффилиация

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