Nonempty types #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file proves a few extra facts about
nonempty, which is defined in core Lean.
Main declarations #
f : α → β, if
α is nonempty then
β is also nonempty.
nonempty cannot be a
functor is restricted to