toFinset_prod

Mathlib.Data.Fintype.Prod

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

← MathLib Explorer

English

If s ⊆ α and t ⊆ β are finite, then (s × t).toFinset equals s.toFinset × t.toFinset.

Русский

Если s ⊆ α и t ⊆ β конечны, то (s × t).toFinset совпадает с s.toFinset × t.toFinset.

LaTeX

$$$(s \\times t).toFinset = s.toFinset \\times t.toFinset$$$

Lean4

theorem toFinset_prod (s : Set α) (t : Set β) [Fintype s] [Fintype t] [Fintype (s ×ˢ t)] :
    (s ×ˢ t).toFinset = s.toFinset ×ˢ t.toFinset := by
  ext
  simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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