English
For any set S, the powerset 𝒫 S = { X ⊆ α | X ⊆ S } is bijectively equivalent to Set S, i.e., the family of subsets of S. There is a natural bijection between subsets of α contained in S and subsets of S.
Русский
Для множества S существует биекция между множеством подмножеств α, заключённых в S, и множеством подмножеств самого S.
LaTeX
$$$𝒫 S \\cong Set S$$$
Lean4
/-- The set `𝒫 S := {x | x ⊆ S}` is equivalent to the type `Set S`. -/
protected def powerset {α} (S : Set α) : 𝒫 S ≃ Set S
where
toFun := fun x : 𝒫 S => Subtype.val ⁻¹' (x : Set α)
invFun := fun x : Set S => ⟨Subtype.val '' x, by rintro _ ⟨a : S, _, rfl⟩; exact a.2⟩
left_inv x := by ext y; exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨_, x.2 h⟩, h, rfl⟩⟩
right_inv x := by ext; simp
