inductionOn₂ — Mathlib

English

Two germs can be handled by a similar induction principle, reducing to representatives.

Русский

Два зародыша по аналогичной индукции сводятся к представлениям.

LaTeX

$$$ \text{inductionOn₂ } (f : \mathrm{Germ}(l, \beta)) (g : \mathrm{Germ}(l, \gamma)) \{p : \mathrm{Germ}(l, \beta) \to \mathrm{Germ}(l, \gamma) \to \text{Prop}\} (h : \forall (f : \alpha \to \beta) (g : \alpha \to \gamma), p(f, g)) : p(f, g)$$$

Lean4

@[elab_as_elim]
theorem inductionOn₂ (f : Germ l β) (g : Germ l γ) {p : Germ l β → Germ l γ → Prop}
    (h : ∀ (f : α → β) (g : α → γ), p f g) : p f g :=
  Quotient.inductionOn₂' f g h

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