lt_and_eval_eq_eval_add_one_of_mem_isAdmissible

English

If L is m-admissible and j ∈ L, then j < m + |L| and the equality of the simplicialEvalσ values holds as above.

Русский

Если L допустим и j ∈ L, то j < m+|L| и выполняется равенство значений simplicialEvalσ.

LaTeX

$$$\\\\text{If } L \\\\text{ is } m\\text{-admissible and } j \\\\in L, \\\\text{ then } j < m + |L| \\\\land \\\\ simplicialEvalσ L j = simplicialEvalσ L (j+1).$$$

Lean4

theorem lt_and_eval_eq_eval_add_one_of_mem_isAdmissible (hL : IsAdmissible m L) (j : ℕ) (hj : j ∈ L) :
    j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L (j + 1) := by
  induction L generalizing m with
  | nil => grind
  | cons a L h_rec =>
    constructor
    · grind [List.mem_iff_getElem, IsAdmissible, List.sorted_cons]
    · obtain rfl | h := List.mem_cons.mp hj
      · grind [simplicialEvalσ_of_lt_mem, simplicialEvalσ, IsAdmissible, List.sorted_cons]
      · have := h_rec hL.tail h
        grind [simplicialEvalσ]

Похожие утверждения