cons — Mathlib

English

The cons operation extends a NormalWord by attaching a new head element in the i-th component, under suitable conditions.

Русский

Операция cons расширяет NormalWord за счет прицепления нового элемента на i-ной компоненте, при соблюдении условий.

LaTeX

$$$ \mathrm{cons}\ g\ w\ hmw\ hgr : \mathrm{NormalWord\ } d \text{ satisfies } \dots $$$

Lean4

/-- A constructor that multiplies a `NormalWord` by an element, with condition to make
sure the underlying list does get longer. -/
@[simps!]
noncomputable def cons {i} (g : G i) (w : NormalWord d) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range) :
    NormalWord d :=
  letI n := (d.compl i).equiv (g * (φ i w.head))
  letI w' :=
    Word.cons (n.2 : G i) w.toWord hmw
      (mt (coe_equiv_snd_eq_one_iff_mem _ (d.one_mem _)).1 (mt (mul_mem_cancel_right (by simp)).1 hgr))
  { toWord := w'
    head := (MonoidHom.ofInjective (d.injective i)).symm n.1
    normalized := fun i g hg => by
      simp only [w', Word.cons, mem_cons, Sigma.mk.inj_iff] at hg
      rcases hg with ⟨rfl, hg | hg⟩
      · simp
      · exact w.normalized _ _ (by assumption) }

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