prod_mono

Mathlib.Data.Set.Prod

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

English

If s1 ⊆ s2 and t1 ⊆ t2, then s1 × t1 ⊆ s2 × t2.

Русский

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

LaTeX

$$$s_1 \\subseteq s_2 \\Rightarrow t_1 \\subseteq t_2 \\Rightarrow s_1 \\times\\! t_1 \\subseteq s_2 \\times\\! t_2$$$

Lean4

@[gcongr]
theorem prod_mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : s₁ ×ˢ t₁ ⊆ s₂ ×ˢ t₂ := fun _ ⟨h₁, h₂⟩ => ⟨hs h₁, ht h₂⟩

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

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

Разделы

Аффилиация

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