English
Let α be finite and p a predicate on α with decidable truth, and assume the subtype {a // p a} is finite. Then projecting the universal subtype to α via the standard inclusion recovers the universal subset: univ.val.map (↑) = (univ.filter p).val.
Русский
Пусть α конечен и p — предикат на α с разрешимой формой, при условии конечности подтипа {a // p a}. Тогда проекция универсума подтипов на α восстанавливает подмножество: univ.val.map (↑) = (univ.filter p).val.
LaTeX
$$$univ.val.map (\iota) = (univ.filter p).val$$$
Lean4
theorem univ_val_map_subtype_val [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a // p a }] :
univ.val.map ((↑) : { a // p a } → α) = (univ.filter p).val :=
by
apply (map_val (Function.Embedding.subtype p) univ).symm.trans
apply congr_arg
apply univ_map_subtype
