Search
❯
Built from ∅ using finitely many pairings and unions.
HF=⋃n<ωVn
x∈HF⟺x finite and ∀y∈x⇒y∈HF