piFinset_nonempty

Mathlib.Data.Fintype.Pi

URI: https://scilib.ai/kg/mathlib#Fintype.piFinset_nonempty

English

piFinset s is nonempty iff every s(a) is nonempty.

Русский

piFinset s непуст тогда и только тогда, когда каждое s(a) непусто.

LaTeX

$$$\\bigl( \\operatorname{piFinset} s \\bigr).\\text{Nonempty} \\iff \\forall a, (s(a)).\\text{Nonempty}.$$$

Lean4

@[simp]
theorem piFinset_nonempty : (piFinset s).Nonempty ↔ ∀ a, (s a).Nonempty := by simp [piFinset]

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

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

Разделы

Аффилиация

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