English
SimplicialInsert preserves admissibility: if L is (m+1)-admissible, then simplicialInsert j L is m-admissible.
Русский
SimplicialInsert сохраняет допустимость: если L (m+1)-допустим, то simplicialInsert j L является m-допустимым.
LaTeX
$$$\\\\text{If } IsAdmissible(m+1,L)\\\\, \\\\text{then } IsAdmissible(m, simplicialInsert(j,L)).$$$
Lean4
/-- `simplicialInsert` preserves admissibility -/
theorem simplicialInsert_isAdmissible (L : List ℕ) (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j < m + 1) :
IsAdmissible m <| simplicialInsert j L := by
induction L generalizing j m with
| nil => constructor <;> simp [simplicialInsert, j.le_of_lt_add_one hj]
| cons a L h_rec =>
dsimp only [simplicialInsert]
split_ifs with ha
· exact .cons _ hL _ (j.le_of_lt_add_one hj) (fun _ ↦ ha)
· refine IsAdmissible.cons _ ?_ _ (not_lt.mp ha |>.trans <| j.le_of_lt_add_one hj) ?_
· refine h_rec _ (.tail a L hL) _ (by simp [hj])
· rw [not_lt, Nat.le_iff_lt_add_one] at ha
intro u
cases L with
| nil => simp [simplicialInsert, ha]
| cons a' l' =>
dsimp only [simplicialInsert]
split_ifs
· exact ha
· exact (List.sorted_cons_cons.mp hL.sorted).1
