isEmpty_prod — Mathlib

English

The product type α × β is empty iff α is empty or β is empty.

Русский

Произведение типов α × β пусто тогда либо α пуст, либо β пуст.

LaTeX

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

Lean4

@[simp]
theorem isEmpty_prod {α β : Type*} : IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β := by
  simp only [← not_nonempty_iff, nonempty_prod, not_and_or]

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