Documentation
Mathlib
.
Data
.
Prod
.
PProd
Search
Google site search
return to top
source
Imports
Init
Mathlib.Logic.Function.Defs
Imported by
PProd
.
mk
.
eta
PProd
.
forall
PProd
.
exists
PProd
.
forall'
PProd
.
exists'
Function
.
Injective
.
pprod_map
Extra facts about
PProd
#
source
@[simp]
theorem
PProd
.
mk
.
eta
{α :
Sort
u_1}
{β :
Sort
u_2}
{p :
PProd
α
β
}
:
⟨
p
.fst
,
p
.snd
⟩
=
p
source
@[simp]
theorem
PProd
.
forall
{α :
Sort
u_1}
{β :
Sort
u_2}
{p :
PProd
α
β
→
Prop
}
:
(
∀ (
x
:
PProd
α
β
),
p
x
)
↔
∀ (
a
:
α
) (
b
:
β
),
p
⟨
a
,
b
⟩
source
@[simp]
theorem
PProd
.
exists
{α :
Sort
u_1}
{β :
Sort
u_2}
{p :
PProd
α
β
→
Prop
}
:
(
∃ (
x
:
PProd
α
β
),
p
x
)
↔
∃ (
a
:
α
),
∃ (
b
:
β
),
p
⟨
a
,
b
⟩
source
theorem
PProd
.
forall'
{α :
Sort
u_1}
{β :
Sort
u_2}
{p :
α
→
β
→
Prop
}
:
(
∀ (
x
:
PProd
α
β
),
p
x
.fst
x
.snd
)
↔
∀ (
a
:
α
) (
b
:
β
),
p
a
b
source
theorem
PProd
.
exists'
{α :
Sort
u_1}
{β :
Sort
u_2}
{p :
α
→
β
→
Prop
}
:
(
∃ (
x
:
PProd
α
β
),
p
x
.fst
x
.snd
)
↔
∃ (
a
:
α
),
∃ (
b
:
β
),
p
a
b
source
theorem
Function
.
Injective
.
pprod_map
{α :
Sort
u_1}
{β :
Sort
u_2}
{γ :
Sort
u_3}
{δ :
Sort
u_4}
{f :
α
→
β
}
{g :
γ
→
δ
}
(hf :
Function.Injective
f
)
(hg :
Function.Injective
g
)
:
Function.Injective
fun (
x
:
PProd
α
γ
) =>
⟨
f
x
.fst
,
g
x
.snd
⟩