inductionOn₂ — Mathlib

English

There is an induction principle on pairs of presented monoid elements: δ(q1, q2) is determined by a base relation on mk rels1 a and mk rels2 b.

Русский

Существует принцип индукции по парам элементов PresentedMonoid: δ(q1, q2) задается базовым отношением на mk rels1 a и mk rels2 b.

LaTeX

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

Lean4

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

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