Theorem RestrictGenTopology.of_nhds

Modification history

2024-11-11 19:06
Mathlib/Topology/RestrictGen.lean
chore(Topology): Namespace `Inducing`, `Embedding`... (#15993) …
Deleted RestrictGenTopology.of_nhdsView on Github →
2024-08-29 08:05
Mathlib/Topology/RestrictGenTopology.lean
feat: the space of continuous maps is complete if the target is complete (#16224)
Added RestrictGenTopology.of_nhdsView on Github →