isEmpty_fun — Mathlib

English

The type of functions α → β is empty iff α is nonempty and β is empty.

Русский

Обозначение функций α → β пусто тогда, когда α непустой и β пустой.

LaTeX

$$IsEmpty(\\alpha \\rightarrow \\beta) \\leftrightarrow \\operatorname{Nonempty}(\\alpha) \\\wedge \\operatorname{IsEmpty}(\\beta)$$

Lean4

theorem isEmpty_fun : IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β := by
  rw [isEmpty_pi, ← exists_true_iff_nonempty, ← exists_and_right, true_and]

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