English
Let α be finite and p a predicate on α with decidable truth, and assume the subtype {a // p a} is finite. Then mapping the universal Finset along the subtype embedding yields the universal Finset filtered by p: univ.map (Embedding.subtype p) = univ.filter p.
Русский
Пусть α конечен и p — предикат на α с разрешимой формой. Тогда отображение универсума через вложение подтипа даёт универсуем, отфильтрованный по p: univ.map (Embedding.subtype p) = univ.filter p.
LaTeX
$$$\operatorname{univ}.map (\operatorname{Function.Embedding.subtype}~p) = \operatorname{univ}.filter p$$$
Lean4
theorem univ_map_subtype [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a // p a }] :
univ.map (Function.Embedding.subtype p) = univ.filter p := by rw [← subtype_map, subtype_univ]
