induction_on — Mathlib

English

Let motive be a property defined on elements of the HNN extension. If it holds for all images of g ∈ G via the natural map of (of g), it holds for the distinguished element t, is closed under multiplication, and closed under inverse, then motive holds for every element of the HNN extension.

Русский

Пусть свойство motive определяется на элементах HNN-расширения. Если оно выполняется для всех элементов, получаемых из g через естественное вложение of g, при этом выполняются условия для t и свойство сохраняется при умножении и взятии обратного, то motive выполняется для каждого элемента HNN-расширения.

LaTeX

$$$\\text{If } motive: HNN(G,A,B,\\varphi) \\to \\mathsf{Prop} \\text{ satisfies } motive(\\mathrm{of}(g)) \\text{ for all } g,\\; motive(t),\\; motive(x) \\Rightarrow motive(xy)\\text{ and } motive(x^{-1}), \\text{ then } motive(x) \\text{ for all } x. $$$

Lean4

@[elab_as_elim]
theorem induction_on {motive : HNNExtension G A B φ → Prop} (x : HNNExtension G A B φ) (of : ∀ g, motive (of g))
    (t : motive t) (mul : ∀ x y, motive x → motive y → motive (x * y)) (inv : ∀ x, motive x → motive x⁻¹) : motive x :=
  by
  let S : Subgroup (HNNExtension G A B φ) :=
    { carrier := setOf motive
      one_mem' := by simpa using of 1
      mul_mem' := mul _ _
      inv_mem' := inv _ }
  let f : HNNExtension G A B φ →* S :=
    lift (HNNExtension.of.codRestrict S of) ⟨HNNExtension.t, t⟩ (by intro a; ext; simp [equiv_eq_conj, mul_assoc])
  have hf : S.subtype.comp f = MonoidHom.id _ := hom_ext (by ext; simp [f]) (by simp [f])
  change motive (MonoidHom.id _ x)
  rw [← hf]
  exact (f x).2

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