mathlib3
dae1dfe9 - feat(topology/spectral/hom): Spectral maps (#12228)

Commit
3 years ago
feat(topology/spectral/hom): Spectral maps (#12228) Define spectral maps in three ways: * `is_spectral_map`, the unbundled predicate * `spectral_map`, the bundled type * `spectral_map_class`, the hom class The design for `is_spectral_map` matches `continuous`. The design for `spectral_map` and `spectral_map_class` follows the hom refactor.
Author
Parents
Loading