isEmpty_pprod — Mathlib

English

The dependent product PProd α β is empty iff α is empty or β is empty.

Русский

Зависимое произведение PProd α β пусто тогда, когда α пусто или β пусто.

LaTeX

$$IsEmpty(\\PProd\\{\\alpha\\,\\beta\\}) \\leftrightarrow \\IsEmpty(\\alpha) \\lor \\ IsEmpty(\\beta)$$

Lean4

@[simp]
theorem isEmpty_pprod : IsEmpty (PProd α β) ↔ IsEmpty α ∨ IsEmpty β := by
  simp only [← not_nonempty_iff, nonempty_pprod, not_and_or]

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