English
Induction up to the universe: for finite α, if S0 ⊆ univ and H0: C S0 and H1: for all S ≠ univ, C S → ∃ a ∉ S, C(insert a S), then C(univ).
Русский
Индукция вплоть до множества-единицы: при конечном α, если S0 ⊆ унив, и C S0 и для всех S ≠ унив, C S ⇒ существует a ∉ S и C (S ∪ {a}), то C(univ).
LaTeX
$$$[Finite\\;\\alpha] \\Rightarrow C(S_0) \\Rightarrow (\\forall S \\neq \\mathrm{univ}, C(S) \\Rightarrow \\exists a \\notin S, C(S \\cup \\{a\\})) \\Rightarrow C(\\mathrm{univ})$$$
Lean4
/-- Induction up to `univ`. -/
theorem induction_to_univ [Finite α] {C : Set α → Prop} (S0 : Set α) (H0 : C S0)
(H1 : ∀ S ≠ univ, C S → ∃ a ∉ S, C (insert a S)) : C univ :=
finite_univ.induction_to S0 (subset_univ S0) H0 (by simpa [ssubset_univ_iff])
