English
For any predicate p on Finset α, (for all Finsets s, p(s)) iff (for all finite sets S, p(S.toFinset)).
Русский
Для любого предиката p на Finset α справедливость: (для всех Finset, p) эквивалентна (для всех конечных множеств, p(S.toFinset)).
LaTeX
$$$\\forall p:\\mathrm{Finset}(\\alpha) \\to \\mathrm{Prop},\\; \\Bigl(\\forall s:\\mathrm{Finset}(\\alpha),\\; p(s)\\Bigr) \\iff \\Bigl(\\forall S:\\mathrm{Set}(\\alpha),\\; S\\text{ finite} \\Rightarrow p(S^{\\text{toFinset}})\\Bigr).$$$
Lean4
/-- This is a kind of induction principle. See `Finset.induction` for the usual induction principle
for finsets. -/
theorem «forall» {p : Finset α → Prop} : (∀ s, p s) ↔ ∀ (s : Set α) (hs : s.Finite), p hs.toFinset
where
mp h s hs := h _
mpr h s := by simpa using h s s.finite_toSet
