product_subset_product_left

Mathlib.Data.Finset.Prod

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

English

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

Русский

Если s ⊆ s', то s ×ˢ t ⊆ s' ×ˢ t для любого t.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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