English
If hs shows that s is well-founded under r, and x ∈ s, then for any predicate P, if for every y ∈ s, whenever all z ∈ s with r z y satisfy P z, then P y, then P x.
Русский
Если s хорошо основано по r и x ∈ s, то для любого предиката P, если для каждого y ∈ s истинно: если для всех z ∈ s с r z y выполняется P z, то P y, то P x.
LaTeX
$$hs : s.WellFoundedOn r → hx : x ∈ s → ∀ P: α → Prop, (∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y) → P x$$
Lean4
protected theorem induction (hs : s.WellFoundedOn r) (hx : x ∈ s) {P : α → Prop}
(hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y) : P x :=
by
let Q : s → Prop := fun y => P y
change Q ⟨x, hx⟩
refine WellFounded.induction hs ⟨x, hx⟩ ?_
simpa only [Subtype.forall]
