fst

Mathlib.Data.Finset.Prod

URI: https://scilib.ai/kg/mathlib#Finset.Nonempty.fst

English

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

Русский

Если произведение s × t не пусто, то s не пусто.

LaTeX

$$$(s \\\\times t) \\\\neq \\\\emptyset \Rightarrow s \\\\neq \\\\emptyset$$$

Lean4

theorem fst (h : (s ×ˢ t).Nonempty) : s.Nonempty :=
  let ⟨xy, hxy⟩ := h
  ⟨xy.1, (mem_product.1 hxy).1⟩

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

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

Разделы

Аффилиация

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