subset_product_image_snd

Mathlib.Data.Finset.Prod

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

English

The set of second components of elements of s ×ˢ t is contained in t.

Русский

Множество вторых компонент пар из s × t содержится в t.

LaTeX

$$$(s \timesˢ t).\mathrm{image}\mathrm{snd} \subseteq t$$$

Lean4

theorem subset_product_image_snd [DecidableEq β] : (s ×ˢ t).image Prod.snd ⊆ t := fun i => by
  simp +contextual [mem_image]

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

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

Разделы

Аффилиация

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