simplicialEvalσ_of_lt_mem — Mathlib

English

If L is admissible and j satisfies a strong bound j ≤ k for all k ∈ L, then simplicialEvalσ L j = j.

Русский

Если L допустим и для всех k∈L справедливо j ≤ k, то simplicialEvalσ L j = j.

LaTeX

$$$\\\\text{If } h_L \\,:\\ IsAdmissible(m,L) \\\\text{ and } (\\\\forall k \in L)\\, j \\le k, \\\\text{then } \\\\text{simplicialEvalσ}(L,j)=j.$$$

Lean4

theorem simplicialEvalσ_of_lt_mem (j : ℕ) (hj : ∀ k ∈ L, j ≤ k) : simplicialEvalσ L j = j := by
  induction L with
  | nil => grind [simplicialEvalσ]
  | cons _ _ _ =>
    simp only [List.mem_cons, forall_eq_or_imp] at hj
    grind [simplicialEvalσ]

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