Documentation
Projects
.
AP
.
Defense
.
Edge
.
Symmetry
.
Basic
Search
return to top
source
Imports
Init
Projects.AP.Defense.Edge.Basic
Imported by
AP
.
Edge
.
vert_dir_of_hor
AP
.
Edge
.
not_hor_dir_of_hor
AP
.
Edge
.
hor_dir_of_vert
AP
.
Edge
.
not_vert_dir_of_vert
AP
.
Edge
.
dir_eq_of_up
AP
.
Edge
.
dir_eq_of_down
AP
.
Edge
.
hor_of_up
AP
.
Edge
.
not_vert_of_up
AP
.
Edge
.
hor_of_down
AP
.
Edge
.
instFactHorOfEqDirDirUp
AP
.
Edge
.
dir_eq_or_eq_of_hor
source
@[simp]
theorem
AP
.
Edge
.
vert_dir_of_hor
{
e
:
Edge
}
[
H
:
Fact
e
.
hor
]
:
e
.
dir
.
vert
source
@[simp]
theorem
AP
.
Edge
.
not_hor_dir_of_hor
{
e
:
Edge
}
[
H
:
Fact
e
.
hor
]
:
¬
e
.
dir
.
hor
source
@[simp]
theorem
AP
.
Edge
.
hor_dir_of_vert
{
e
:
Edge
}
[
H
:
Fact
e
.
vert
]
:
e
.
dir
.
hor
source
@[simp]
theorem
AP
.
Edge
.
not_vert_dir_of_vert
{
e
:
Edge
}
[
H
:
Fact
e
.
vert
]
:
¬
e
.
dir
.
vert
source
@[simp]
theorem
AP
.
Edge
.
dir_eq_of_up
{
e
:
Edge
}
[
H
:
Fact
(
e
.
dir
=
Dir.up
)
]
:
e
.
dir
=
Dir.up
source
@[simp]
theorem
AP
.
Edge
.
dir_eq_of_down
{
e
:
Edge
}
[
H
:
Fact
(
e
.
dir
=
Dir.down
)
]
:
e
.
dir
=
Dir.down
source
@[simp]
theorem
AP
.
Edge
.
hor_of_up
{
e
:
Edge
}
[
H
:
Fact
(
e
.
dir
=
Dir.up
)
]
:
e
.
hor
source
@[simp]
theorem
AP
.
Edge
.
not_vert_of_up
{
e
:
Edge
}
[
H
:
Fact
(
e
.
dir
=
Dir.up
)
]
:
¬
e
.
vert
source
@[simp]
theorem
AP
.
Edge
.
hor_of_down
{
e
:
Edge
}
[
H
:
Fact
(
e
.
dir
=
Dir.down
)
]
:
e
.
hor
source
@[simp]
instance
AP
.
Edge
.
instFactHorOfEqDirDirUp
{
e
:
Edge
}
[
H
:
Fact
(
e
.
dir
=
Dir.up
)
]
:
Fact
e
.
hor
source
@[simp]
theorem
AP
.
Edge
.
dir_eq_or_eq_of_hor
{
e
:
Edge
}
[
H
:
Fact
e
.
hor
]
:
e
.
dir
=
Dir.up
∨
e
.
dir
=
Dir.down