feat(topology/stone_cech): add stone_cech_hom_ext (#13472)
The universal property that characterises the Stone–Čech compactification of a topological space X is that any function from X to a compact Hausdorff space extends uniquely to a continuous function on βX. Existence is already provided by `unique_stone_cech_extend`, but it seems that the uniqueness lemma was intentionally omitted previously. Easy, but probably worth being explicit about.
Co-authored-by: Matias Heikkilä <matias@three.consulting>
