Documentation
Foundation
.
Vorspiel
.
IsEmpty
Search
return to top
source
Imports
Init
Mathlib.Logic.IsEmpty.Basic
Imported by
IsEmpty
.
eq_elim'
IsEmpty
.
eq_elim
source
theorem
IsEmpty
.
eq_elim'
{
o
:
Sort
u}
(
h
:
IsEmpty
o
)
{
α
:
Sort
u_1}
(
f
:
o
→
α
)
:
f
=
h
.
elim'
source
theorem
IsEmpty
.
eq_elim
{
o
:
Sort
u}
(
h
:
IsEmpty
o
)
{
α
:
Sort
u_1}
(
f
:
o
→
α
)
:
f
=
fun (
a
:
o
) =>
h
.
elim
a