Documentation
Foundation
.
Vorspiel
.
Empty
Search
return to top
source
Imports
Init
Mathlib.Data.Fintype.Basic
Imported by
Empty
.
eq_elim
source
theorem
Empty
.
eq_elim
{
α
:
Sort
u}
(
f
:
Empty
→
α
)
:
f
=
elim