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