English
Let P be a property of Part α. If P none holds and P(some a) holds for all a, then P(a) holds for every a ∈ Part α. This is the induction principle for Part.
Русский
Пусть P — свойство Part α. Если P(none) верно и P(some a) верно для каждого a, то P(a) верно для любого a ∈ Part α. Это индукция по Part.
LaTeX
$$$ \forall P : \mathrm{Part}(\alpha) \rightarrow \mathrm{Prop},\ a : \mathrm{Part}(\alpha),\ P(\mathrm{none}) \rightarrow (\\forall x : \alpha, P(\\mathrm{some } x)) \rightarrow P(a) $$$
Lean4
@[elab_as_elim]
protected theorem induction_on {P : Part α → Prop} (a : Part α) (hnone : P none) (hsome : ∀ a : α, P (some a)) : P a :=
(Classical.em a.Dom).elim (fun h => Part.some_get h ▸ hsome _) fun h => (eq_none_iff'.2 h).symm ▸ hnone
