English
Let x be an element of PerfectClosure(K, p). For any property Q on PerfectClosure(K, p), if Q holds for mk(K, p, z) for every z ∈ N × K, then Q(x) holds. This is the induction principle for PerfectClosure.
Русский
Пусть x принадлежит PerfectClosure(K, p). Для любого свойства Q над PerfectClosure(K, p), если Q выполняется для mk(K, p, z) для каждого z ∈ N × K, тогда Q(x) выполняется. Это принцип индукции для PerfectClosure.
LaTeX
$$$\\forall K [\\text{CommRing }K], p [\\text{Prime }p], [\\text{CharP }K p], x:\\ PerfectClosure(K,p), {\\} Q:\\ PerfectClosure(K,p) \\to \\mathrm{Prop}, (\\forall z: \\mathbb{N} \\times K, Q(\\mathrm{mk}\\,K\\,p\,z)) \\to Q(x)$$$
Lean4
@[elab_as_elim]
theorem induction_on (x : PerfectClosure K p) {q : PerfectClosure K p → Prop} (h : ∀ x, q (mk K p x)) : q x :=
Quot.inductionOn x h
