English
Let I be a type and P a predicate on functions from I to Cardinal. For a fixed f: I → Cardinal, if P holds for every family of types A_i indexed by I in the form i ↦ #(A_i), then P holds for f. More precisely, if for every f : I → Type v the statement P( i ↦ #(f i) ) holds, then P(f) holds.
Русский
Пусть I — тип, P — предикат над функциями I → Кардинал. Для фиксированной функции f: I → Кардинал, если P выполняется для любой семейства типов A_i (индексируемого по I) в виде i ↦ #(A_i), то P выполняется для f. Точнее: если ∀ A : I → Type v выполнено P( i ↦ #(A i) ), то P(f).
LaTeX
$$$\\forall f:\\, \\iota \\to \\mathrm{Cardinal},\\; (\\forall A:\\, \\iota \\to \\mathrm{Type}_v,\\; P(\\lambda i:\\, \\iota.\\ #(A i))) \\Rightarrow P f$$$
Lean4
theorem induction_on_pi {ι : Type u} {p : (ι → Cardinal.{v}) → Prop} (f : ι → Cardinal.{v})
(h : ∀ f : ι → Type v, p fun i ↦ #(f i)) : p f :=
Quotient.induction_on_pi f h
