note-math

the original inspiration of compactness: The intersection of closed interval nets of is non-empty closed_interval_net_theorem

is a limit point of of . The net seems to converge to

But

Compare the multiplicative inverse’s

does not have corresponding to the possible limit

Compare

let topological space. let

[compact] compact := forall net of , exists , forall , forall ,

Meaning: The elements of any net have a common limit point under the topology . Or, after closure, the net converges to a non-empty set or the intersection is non-empty, instead of converging to the empty set (e.g., Euclidean converges to the empty set or converges to infinity, but there are many other complex situations)

By using the equivalent limit <==> image net finer, compact can also be represented by replacing any net of with any source_net_space -> target_topology_space function. Although this introduces an “extra” domain source_net_space

According to the definitions of limit points and closed sets, compact is equivalent to: forall net of ,

Any net can replenish all finite intersections and maintain the same limit, so for compact, the equivalent description is

compact <==>

logically equivalent to

logically equivalent to [compact_finite_open_cover]

[compact_subset] := topology_subspace compact

recall closed_in_subspace, , denoted as

compact-subset logically equivalent to

logically equivalent to

logically equivalent to [compact_subset_finite_open_cover]

compact-subset is closed under finite unions. this is easy to proof

[closed_set_in_compact_space_is_compact] compact and closed ==> compact

Proof

Hausdorff space :=

Hausdorff + compact ==> closed. At this time, compact is closed for any intersection

[continous_preserve_compact] let . is compact-subset of

Proof

Contrapositive: Under a continuous function, the inverse image of non-compact is non-compact

[quotient_topology_preserve_compact] For quotient_topology , source space compact ==> quotient space compact. because the quotient map is continuous, it preserves compact

[product_topology_preserve_compact] product_topology preserves compact

Proof