snd

Mathlib.Data.Finset.Prod

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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