isEmpty_pi

Mathlib.Logic.IsEmpty

URI: https://scilib.ai/kg/mathlib#isEmpty_pi

← MathLib Explorer

English

IsEmpty (∀ a, π(a)) iff ∃ a, IsEmpty (π(a)).

Русский

Пустой Pi-тип: IsEmpty(∀ a, π(a)) эквивалентно ∃ a, IsEmpty(π(a)).

LaTeX

$$IsEmpty(\\forall a:\\alpha,\\;\\pi(a)) \\leftrightarrow \\exists a:\\alpha, IsEmpty(\\pi(a))$$

Lean4

@[simp]
theorem isEmpty_pi {π : α → Sort*} : IsEmpty (∀ a, π a) ↔ ∃ a, IsEmpty (π a) := by
  simp only [← not_nonempty_iff, Classical.nonempty_pi, not_forall]

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

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

Разделы

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

Аффилиация

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