subset_product_image_fst

Mathlib.Data.Finset.Prod

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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