English
There is a natural equivalence between Finset of subtypes {a ∈ α | p a} and Finset of α together with a proof that all elements satisfy p.
Русский
Существует естественная эквивалентность между Finset подтипов {a ∈ α | p a} и Finset α с доказательством того, что все элементы удовлетворяют p.
LaTeX
$$$\\mathrm{Finset}\\bigl\\{a\\in\\alpha\\mid p(a)\\bigr\\} \\ ≃\\ {s:\\mathrm{Finset}\\alpha\\;|\\;\\forall a\\in s, p(a)}$$$
Lean4
/-- Given a predicate `p : α → Prop`, produces an equivalence between
`Finset {a : α // p a}` and `{s : Finset α // ∀ a ∈ s, p a}`. -/
@[simps]
protected def finsetSubtypeComm (p : α → Prop) : Finset { a : α // p a } ≃ { s : Finset α // ∀ a ∈ s, p a }
where
toFun
s :=
⟨s.map ⟨fun a ↦ a.val, Subtype.val_injective⟩, fun _ h ↦
have ⟨v, _, h⟩ := Embedding.coeFn_mk _ _ ▸ mem_map.mp h;
h ▸ v.property⟩
invFun s := s.val.attach.map (Subtype.impEmbedding _ _ s.property)
left_inv
s := by ext a;
constructor <;> intro h <;>
simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk, exists_and_right,
exists_eq_right, Subtype.impEmbedding] at * <;>
grind
right_inv
s := by ext a;
constructor <;> intro h <;>
simp only [Finset.mem_map, Finset.mem_attach, Subtype.exists, Embedding.coeFn_mk, Subtype.impEmbedding] at * <;>
grind
