inductionOn₃ — Mathlib

English

There is an induction principle on triples of presented monoid elements: δ(q1, q2, q3) follows from base relations on each mk rels i.

Русский

Существует индукционный принцип по тройкам элементов PresentedMonoid: δ(q1, q2, q3) следует из базовых отношений на каждом mk rels i.

LaTeX

$$$\\forall q_1 q_2 q_3, \\delta(q_1,q_2,q_3) \\text{ if } \\forall a,b,c, δ(\\mathrm{mk}\\ rels_1\, a)(\\mathrm{mk}\\ rels_2\, b)(\\mathrm{mk}\\ rels_3\, c)$$$

Lean4

@[to_additive (attr := elab_as_elim)]
protected theorem inductionOn₃ {δ : P₁ → P₂ → P₃ → Prop} (q₁ : P₁) (q₂ : P₂) (q₃ : P₃)
    (h : ∀ a b c, δ (mk rels₁ a) (mk rels₂ b) (mk rels₃ c)) : δ q₁ q₂ q₃ :=
  Quotient.inductionOn₃ q₁ q₂ q₃ h

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