English
There is a natural equivalence between the set of elements of α with property p and the collection of subsets s ⊆ α with ∀ a ∈ s, p a.
Русский
Существует естественное эквивалентное отображение между множеством элементов α с свойством p и множеством подмножеств s ⊆ α, удовлетворяющих ∀ a ∈ s, p a.
LaTeX
$$$ Set\\bigl\\{ a : α \\mid p(a) \\bigr\\} \\simeq \\{ s : Set α \\mid \\forall a \\in s, p(a) \\}$$$
Lean4
/-- Given a predicate `p : α → Prop`, produces an equivalence between
`Set {a : α // p a}` and `{s : Set α // ∀ a ∈ s, p a}`. -/
protected def setSubtypeComm (p : α → Prop) : Set { a : α // p a } ≃ { s : Set α // ∀ a ∈ s, p a }
where
toFun s := ⟨{a | ∃ h : p a, s ⟨a, h⟩}, fun _ h ↦ h.1⟩
invFun s := {a | a.val ∈ s.val}
left_inv s := by ext a; exact ⟨fun h ↦ h.2, fun h ↦ ⟨a.property, h⟩⟩
right_inv s := by ext; exact ⟨fun h ↦ h.2, fun h ↦ ⟨s.property _ h, h⟩⟩
