Types that are empty #
In this file we define a typeclass IsEmpty
, which expresses that a type has no elements.
Main declaration #
IsEmpty
: a typeclass that expresses that a type is empty.
theorem
Function.Surjective.isEmpty
{α : Sort u_1}
{β : Sort u_2}
[IsEmpty α]
{f : α → β}
(hf : Surjective f)
:
IsEmpty β
Non-dependent version of IsEmpty.elim
. Helpful if the elaborator cannot elaborate h.elim a
correctly.
Equations
Instances For
@[simp]
@[simp]