HepLean Documentation
Init
.
Data
.
List
.
Nat
.
Erase
Search
Google site search
return to top
source
Imports
Init.Data.List.Erase
Init.Data.List.Nat.TakeDrop
Imported by
List
.
getElem?_eraseIdx
List
.
getElem?_eraseIdx_of_lt
List
.
getElem?_eraseIdx_of_ge
List
.
getElem_eraseIdx
List
.
getElem_eraseIdx_of_lt
List
.
getElem_eraseIdx_of_ge
source
theorem
List
.
getElem?_eraseIdx
{α :
Type
u_1}
(l :
List
α
)
(i j :
Nat
)
:
(
l
.eraseIdx
i
)
[
j
]?
=
if
j
<
i
then
l
[
j
]?
else
l
[
j
+
1
]?
source
theorem
List
.
getElem?_eraseIdx_of_lt
{α :
Type
u_1}
(l :
List
α
)
(i j :
Nat
)
(h :
j
<
i
)
:
(
l
.eraseIdx
i
)
[
j
]?
=
l
[
j
]?
source
theorem
List
.
getElem?_eraseIdx_of_ge
{α :
Type
u_1}
(l :
List
α
)
(i j :
Nat
)
(h :
i
≤
j
)
:
(
l
.eraseIdx
i
)
[
j
]?
=
l
[
j
+
1
]?
source
theorem
List
.
getElem_eraseIdx
{α :
Type
u_1}
(l :
List
α
)
(i j :
Nat
)
(h :
j
<
(
l
.eraseIdx
i
)
.length
)
:
(
l
.eraseIdx
i
)
[
j
]
=
if h' :
j
<
i
then
l
[
j
]
else
l
[
j
+
1
]
source
theorem
List
.
getElem_eraseIdx_of_lt
{α :
Type
u_1}
(l :
List
α
)
(i j :
Nat
)
(h :
j
<
(
l
.eraseIdx
i
)
.length
)
(h' :
j
<
i
)
:
(
l
.eraseIdx
i
)
[
j
]
=
l
[
j
]
source
theorem
List
.
getElem_eraseIdx_of_ge
{α :
Type
u_1}
(l :
List
α
)
(i j :
Nat
)
(h :
j
<
(
l
.eraseIdx
i
)
.length
)
(h' :
i
≤
j
)
:
(
l
.eraseIdx
i
)
[
j
]
=
l
[
j
+
1
]