instIsEmptyForallOfNonempty — Mathlib

English

Subtypes on an empty ambient type are empty; more precisely, if for all x, p x holds in an empty ambient, then the universal quantification is empty.

Русский

Подтипы пустого типа пусты; если для всех x выполняется p x, то функция 1-1 не существует.

LaTeX

$$$ [\forall x, IsEmpty(p x)] [\text{Nonempty } \alpha] : IsEmpty(\forall x, p x) $$$

Lean4

instance {p : α → Sort*} [∀ x, IsEmpty (p x)] [h : Nonempty α] : IsEmpty (∀ x, p x) :=
  h.elim fun x ↦ Function.isEmpty <| Function.eval x

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