Def TopologicalSpace.OpenNhds.infLELeft

Modification history

2023-05-16 13:10
Mathlib/Topology/Category/Top/OpenNhds.lean
chore: tidy various files (#4003)
Added TopologicalSpace.OpenNhds.infLELeftView on Github →