consRecOn — Mathlib

English

Same compatibility as above, with explicit statement that cons applied to the composed word equals the composed cons applied to components.

Русский

Та же совместимость, что и выше: применение cons к композиции слова равно композиции применений cons к частям.

LaTeX

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

Lean4

/-- A recursor to induct on a `NormalWord`, by proving the property is preserved under `cons` -/
@[elab_as_elim]
def consRecOn {motive : NormalWord d → Sort*} (w : NormalWord d) (ofGroup : ∀ g, motive (ofGroup g))
    (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'),
        motive w → motive (cons g u w h1 h2)) :
    motive w := by
  rcases w with ⟨⟨g, l, chain⟩, mem_set⟩
  induction l generalizing g with
  | nil => exact ofGroup _
  | cons a l ih =>
    exact
      cons g a.1
        { head := a.2
          toList := l
          mem_set := fun _ _ h => mem_set _ _ (List.mem_cons_of_mem _ h), chain := (List.isChain_cons'.1 chain).2 }
        (mem_set a.1 a.2 List.mem_cons_self) (by simpa using (List.isChain_cons'.1 chain).1) (ih _ _ _)

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