HepLean Documentation
Init
.
Data
.
Subtype
Search
Google site search
return to top
source
Imports
Init.Ext
Imported by
Subtype
.
ext
Subtype
.
forall
Subtype
.
exists
source
theorem
Subtype
.
ext
{α :
Sort
u}
{p :
α
→
Prop
}
{a1 a2 :
{
x
:
α
//
p
x
}
}
:
a1
.val
=
a2
.val
→
a1
=
a2
source
@[simp]
theorem
Subtype
.
forall
{α :
Sort
u}
{p :
α
→
Prop
}
{q :
{
a
:
α
//
p
a
}
→
Prop
}
:
(∀ (
x
:
{
a
:
α
//
p
a
}
),
q
x
)
↔
∀ (
a
:
α
) (
b
:
p
a
),
q
⟨
a
,
b
⟩
source
@[simp]
theorem
Subtype
.
exists
{α :
Sort
u}
{p :
α
→
Prop
}
{q :
{
a
:
α
//
p
a
}
→
Prop
}
:
(∃ (
x
:
{
a
:
α
//
p
a
}
),
q
x
)
↔
∃ (
a
:
α
),
∃ (
b
:
p
a
),
q
⟨
a
,
b
⟩