English
Given a predicate p on α represented by a finite set s with H : ∀ x, x ∈ s ↔ p x, the subtype { x // p x } is a fintype.
Русский
Если предикат p на α задан конечным множеством s с условием H, то подтип { x // p x } является fintype.
LaTeX
$$$$ \exists s: \mathrm{Finset} \; \alpha, (\forall x, x \in s \iff p x) \Rightarrow \mathrm{Fintype}\;\{ x \mid p x \} $$$$
Lean4
/-- Given a predicate that can be represented by a finset, the subtype
associated to the predicate is a fintype. -/
protected def subtype {p : α → Prop} (s : Finset α) (H : ∀ x : α, x ∈ s ↔ p x) : Fintype { x // p x } :=
⟨⟨s.1.pmap Subtype.mk fun x => (H x).1, s.nodup.pmap fun _ _ _ _ => congr_arg Subtype.val⟩, fun ⟨x, px⟩ =>
Multiset.mem_pmap.2 ⟨x, (H x).2 px, rfl⟩⟩
