Documentation
Projects
.
Util
.
Prod
Search
return to top
source
Imports
Init
Projects.Util.Logic
Imported by
Prod
.
fst_eq_of_eq_mk
Prod
.
snd_eq_of_eq_mk
source
theorem
Prod
.
fst_eq_of_eq_mk
{
α
:
Type
u_1}
{
β
:
Type
u_2}
{
a
:
α
×
β
}
{
x
:
α
}
{
y
:
β
}
(
h
:
a
=
(
x
,
y
)
)
:
x
=
a
.1
source
theorem
Prod
.
snd_eq_of_eq_mk
{
α
:
Type
u_1}
{
β
:
Type
u_2}
{
a
:
α
×
β
}
{
x
:
α
}
{
y
:
β
}
(
h
:
a
=
(
x
,
y
)
)
:
y
=
a
.2