English
Three germs admit a joint induction principle via representatives.
Русский
Три зародыша обладают общим принципом индукции через представители.
LaTeX
$$$ \text{inductionOn₃ } (f : \mathrm{Germ}(l, \beta)) (g : \mathrm{Germ}(l, \gamma)) (h : \mathrm{Germ}(l, \delta)) \\ {p : \mathrm{Germ}(l, \beta) \to \mathrm{Germ}(l, \gamma) \to \mathrm{Germ}(l, \delta) \to \text{Prop}} (H : \forall (f : \alpha \to \beta) (g : \alpha \to \gamma) (h : \alpha \to \delta), p(f, g, h)) : p(f, g, h)$$$
Lean4
@[elab_as_elim]
theorem inductionOn₃ (f : Germ l β) (g : Germ l γ) (h : Germ l δ) {p : Germ l β → Germ l γ → Germ l δ → Prop}
(H : ∀ (f : α → β) (g : α → γ) (h : α → δ), p f g h) : p f g h :=
Quotient.inductionOn₃' f g h H
