English
Let α be a finite type and p a predicate on α with decidable truth. If the subtype {a ∈ α | p a} is finite, then the Finset of all a ∈ α with p, viewed as elements of the subtype, equals the universal Finset of that subtype: univ.subtype p = univ.
Русский
Пусть α — конечного типа и p — предикат на α с разрешимым доказательством. При условии, что подтип {a ∈ α | p a} конечен, множество элементов α, удовлетворяющих p, рассмотренное как подп Finset данного подтипа, совпадает с полным Finset этого подтипа: univ.subtype p = univ.
LaTeX
$$$univ.subtype\ p = univ$$$
Lean4
@[simp]
theorem subtype_univ [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a // p a }] : univ.subtype p = univ := by
simp
