of_prod_left

Mathlib.Data.Finite.Prod

URI: https://scilib.ai/kg/mathlib#Set.Finite.of_prod_left

← MathLib Explorer

English

If s × t is finite and t is nonempty, then s is finite.

Русский

Если s × t конечно и t непусто, то s конечно.

LaTeX

$$$ (s \\timesˢ t).Finite \\Rightarrow t.Nonempty \\Rightarrow s.Finite $$$

Lean4

theorem of_prod_left (h : (s ×ˢ t : Set (α × β)).Finite) : t.Nonempty → s.Finite := fun ⟨b, hb⟩ =>
  (h.image Prod.fst).subset fun a ha => ⟨(a, b), ⟨ha, hb⟩, rfl⟩

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

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

Разделы

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

Аффилиация

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