Def TopologicalSpace.OpenNhdsOf.comap

Modification history

2023-02-11 07:51

Mathlib/Topology/Sets/Opens.lean

feat: port Topology.Sets.Opens (#2118)

Added TopologicalSpace.OpenNhdsOf.comap View on Github →