cons — Mathlib

English

The recursive construction is compatible: applying cons to a word built by cons with parameters yields the same as applying cons to the original arguments.

Русский

Рекурсивная конструкция совместима: применение cons к слову, построенному через cons с параметрами, даёт то же, что и применение cons к исходным аргументам.

LaTeX

$$$\\mathrm{consRecOn}(\\mathrm{cons}\\ g\\ u\\ w\\ h_1\\ h_2) \\; = \\; \\mathrm{cons}(g,u,w,h_1,h_2)\\,$$

Lean4

/-- A constructor to append an element `g` of `G` and `u : ℤˣ` to a word `w` with sufficient
hypotheses that no normalization or cancellation need take place for the result to be in normal form
-/
@[simps]
def cons (g : G) (u : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u)
    (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') : NormalWord d :=
  { head := g, toList := (u, w.head) :: w.toList,
    mem_set := by
      intro u' g' h'
      simp only [List.mem_cons, Prod.mk.injEq] at h'
      rcases h' with ⟨rfl, rfl⟩ | h'
      · exact h1
      · exact w.mem_set _ _ h'
    chain := by
      refine List.isChain_cons'.2 ⟨?_, w.chain⟩
      rintro ⟨u', g'⟩ hu' hw1
      exact h2 _ (by simp_all) hw1 }

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