mem_isAdmissible_iff — Mathlib

English

An index j belongs to L exactly when j < m + |L| and simplicialEvalσ L j = simplicialEvalσ L (j+1).

Русский

Индекс j принадлежит L тогда и только тогда, когда j < m+|L| и значения функций совпадают.

LaTeX

$$$\\\\text{j ∈ L} \\\\leftrightarrow \\\\ (j < m + |L|) \\\\land \\\\ simplicialEvalσ L j = simplicialEvalσ L (j+1).$$$

Lean4

/-- We can characterize elements in an admissible list as exactly those for which
`simplicialEvalσ` takes the same value twice in a row. -/
theorem mem_isAdmissible_iff (hL : IsAdmissible m L) (j : ℕ) :
    j ∈ L ↔ j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L (j + 1) := by
  grind [lt_and_eval_eq_eval_add_one_of_mem_isAdmissible, mem_isAdmissible_of_lt_and_eval_eq_eval_add_one]

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