English
Induction principle for TransGen: to prove a property for h : TransGen r a b, it suffices to prove it for single steps and to show closure under transitive concatenation.
Русский
Принцип индукции по TransGen: чтобы доказать свойство для h : TransGen r a b, достаточно доказать для одиночного шага и показать замкнутость при конкатенации транспозиции.
LaTeX
$$$ {motive : \forall {a b}, TransGen r a b \to Prop} {a b} (h : TransGen r a b), (single : \forall {a b} (h : r a b), motive (single h)) \\n (trans : \forall {a b c} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ \to motive h₂ \to motive (h₁.trans h₂)) : motive h $$$
Lean4
@[elab_as_elim]
theorem trans_induction_on {motive : ∀ {a b : α}, TransGen r a b → Prop} {a b : α} (h : TransGen r a b)
(single : ∀ {a b} (h : r a b), motive (single h))
(trans : ∀ {a b c} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive (h₁.trans h₂)) :
motive h := by
induction h with
| single h => exact single h
| tail hab hbc h_ih => exact trans hab (.single hbc) h_ih (single hbc)
