English
There is an equivalence between ZFSet and the small-set subtype of Set ZFSet: ZFSet ≃ { s : Set ZFSet // Small s }.
Русский
Существует эквивалентность между ZFSet и подвессом множества малости: ZFSet ≃ { s : Set ZFSet // Small s }.
LaTeX
$$$ \\mathrm{toSet\\_equiv} : \\mathrm{ZFSet} \\simeq \\{ s : \\mathrm{Set}\\ \\mathrm{ZFSet} \\mid \\mathrm{Small}(s) \\} $.$$
Lean4
/-- `ZFSet.toSet` as an equivalence. -/
@[simps apply_coe]
noncomputable def toSet_equiv : ZFSet.{u} ≃ { s : Set ZFSet.{u} // Small.{u, u + 1} s }
where
toFun x := ⟨x.toSet, x.small_toSet⟩
invFun := fun ⟨s, _⟩ ↦ mk <| PSet.mk (Shrink s) fun x ↦ ((equivShrink.{u, u + 1} s).symm x).1.out
left_inv :=
Function.rightInverse_of_injective_of_leftInverse (by intro _ _; simp) fun s ↦
Subtype.coe_injective <| toSet_equiv_aux s.2
right_inv s := Subtype.coe_injective <| toSet_equiv_aux s.2
