English
Let α be finite and p a predicate on α with decidable truth, and assume the subtype {a // p a} is finite. Then mapping the univ of α through the restricted function to β yields the same as restricting the map by p: univ.val.map (Subtype.restrict p f) = (univ.filter p).val.map f.
Русский
Пусть α конечен и p — предикат на α с разрешимой формой; при условии, что подтип {a // p a} конечен, отображение универсума через ограниченную функцию совпадает с ограниченным отображением: univ.val.map (Subtype.restrict p f) = (univ.filter p).val.map f.
LaTeX
$$$univ.val.map (Subtype.restrict p f) = (univ.filter p).val.map f$$$
Lean4
theorem univ_val_map_subtype_restrict [Fintype α] (f : α → β) (p : α → Prop) [DecidablePred p] [Fintype { a // p a }] :
univ.val.map (Subtype.restrict p f) = (univ.filter p).val.map f := by
rw [← univ_val_map_subtype_val, Multiset.map_map, Subtype.restrict_def]
