English
Given a Finset s of α and a predicate p, the Finset.subtype p s is the Finset of Subtype p consisting of elements of s that satisfy p.
Русский
Для конечного множества s над α и предиката p Finset.subtype p s есть Finset элементов типа Subtype p, которые принадлежат s и удовлетворяют p.
LaTeX
$$$\\mathrm{Finset.subtype}(p,s) = (s.filter\\ p) .attach .map(\\langle \\lambda x, ⟨x.1, \\text{proof}\\rangle, \\lambda _ _ H, \\text{Subtype.eq} \\rangle)$$$
Lean4
/-- Given a finset `s` and a predicate `p`, `s.subtype p` is the finset of `Subtype p` whose
elements belong to `s`. -/
protected def subtype {α} (p : α → Prop) [DecidablePred p] (s : Finset α) : Finset (Subtype p) :=
(s.filter p).attach.map
⟨fun x => ⟨x.1, by simpa using (Finset.mem_filter.1 x.2).2⟩, fun _ _ H => Subtype.eq <| Subtype.mk.inj H⟩
