product_subset_product_right

Mathlib.Data.Finset.Prod

URI: https://scilib.ai/kg/mathlib#Finset.product_subset_product_right

English

If t ⊆ t' then s ×ˢ t ⊆ s ×ˢ t'.

Русский

Если t ⊆ t', то s ×ˢ t ⊆ s ×ˢ t'.

LaTeX

$$$(t \subseteq t') \Rightarrow (s ×ˢ t \subseteq s ×ˢ t')$$$

Lean4

theorem product_subset_product_right (ht : t ⊆ t') : s ×ˢ t ⊆ s ×ˢ t' :=
  product_subset_product (Subset.refl _) ht

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

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

Разделы

Аффилиация

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