English
Let f be a family of quotients f : ∀ i, Quotient (s i) and p a predicate on functions i ↦ Quotient (s i). If for every a : ∀ i, α i we have p (fun i => ⟦a i⟧), then p f.
Русский
Пусть f — семейство квот f : ∀ i, Quotient (s i) и p — предикат на функции i ↦ Quotient (s i). Если для каждого a : ∀ i, α i верно, что p(λ i, ⟦a i⟧), тогда p f.
LaTeX
$$$\\forall f:\\prod_{i} \\mathrm{Quotient}(s(i)),\\; \\Big(\\forall a:\\, \\forall i,\\; p\\, (\\lambda i, \\; \\operatorname{Quotient.mk}(s(i))(a(i)) )\\Big) \\rightarrow p(f)$$$
Lean4
@[elab_as_elim]
theorem induction_on_pi {ι : Type*} {α : ι → Sort*} {s : ∀ i, Setoid (α i)} {p : (∀ i, Quotient (s i)) → Prop}
(f : ∀ i, Quotient (s i)) (h : ∀ a : ∀ i, α i, p fun i ↦ ⟦a i⟧) : p f :=
by
rw [← (funext fun i ↦ Quotient.out_eq (f i) : (fun i ↦ ⟦(f i).out⟧) = f)]
apply h
