nonempty_fun — Mathlib

English

The type α → β is empty exactly when α is nonempty and β is empty.

Русский

Тип функций α → β пуст тогда и только тогда, когда α непустой и β пустой.

LaTeX

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

Lean4

@[simp]
theorem nonempty_fun : Nonempty (α → β) ↔ IsEmpty α ∨ Nonempty β :=
  not_iff_not.mp <| by rw [not_or, not_nonempty_iff, not_nonempty_iff, isEmpty_fun, not_isEmpty_iff]

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