You may not need all of these, but be ready to formalize them as needed:
- assume excluded middle
- define subset of
X
as a mapX → Prop
(powerset ofX
isX → Prop
, this requires{-# OPTIONS --prop #-}
) - show that the powerset is a complete lattice (given any family of subsets, define their union and intersection)
- given
f : X → Y
, define the inverse image mapf^* : P(Y) → P(X)
- direct image map
f_* : P(X) → P(Y)
- subset of a set
- family of subsets
- union of a family of subsets
- inverse image preserves unions and finite intersections
- countable set
- topology on a set
- topology generated by a base (a family of subsets closed under finite intersections)
- the base generated by a subbase (close the subbase under finite intersections)
- examples
- trivial topology
- discrete topology
- partial ordering on the topologies on a set
X
- the trivial topology is the smallest and the discrete topology the largest one
- topologies on a given set form a complete lattice
- the topology generated by a subbasis is the least topology that contains the subbasis
- definition of a continuous map (inverse image preserves opens)
- identity and constant maps are continuous
- composition of continuous maps is continuous
- definition of a homeomorphism
- definition of a subset of a space
- the subspace topology, and its universal property (smallest topology for which inclusion is continuous)
- the product of two spaces, and its univeral property
- the product of a family of spaces, and its universal property
- the coproduct of two spaces, and its universal property
- the coproduct of a family of spaces, and its universal property
- definition of an open cover of a subset
- definition of a subcover
- definition of a finite subcover
- definition of a refinement of a cover
- if the topology of
X
is generated by a basisB
, then every open cover has a refinement consisting of basic open sets
- Hausdorff space
- 2-countable space (the topology is generated by a countable set of opens)
- 0-dimensional space (has a basis of open-closed/clopen subsets)
- compact subset (every open cover has a finite subcover)
- finite subset if compact
- a continuous image of a compact subset is compact
- the compact subsets of a discrete space are the finite subsets
- closed subset of a compact space is compact
- compact subset of a Hausdorff space is closed
- Cantor space 𝕂 (the set ℕ → 2 with product topology)
- 𝕂 is Hausdorff
- 𝕂 is compact
- 𝕂 is 2-countable
- 𝕂 is 0-dimensional
- 𝕂 × K is homeomorphic to 𝕂
- 𝕂 is homogeneous (for any
α, β ∈ 𝕂
there is a homeomorphismh : 𝕂 → 𝕂
such thath α = β
- Sierpinski space (
{⊥, ⊤}
with topology{∅, {⊤}, {⊥, ⊤}}
) - Sierpinski space is
T₀
(if two points have the same neighborhoods then they are equal) - Sierpinski space is compact
- Sierpinski space is not Hausdorff
- Sierpinski space characterizes open sets (continuous maps
X → 𝕊
are in bijective correspondence with open subsets ofX
)