Def TopologicalSpace.OpenNhds.infLeLeft

Modification history

2023-05-16 13:10
Mathlib/Topology/Category/Top/OpenNhds.lean
chore: tidy various files (#4003)
Deleted TopologicalSpace.OpenNhds.infLeLeftView on Github →
2023-05-08 02:51
Mathlib/Topology/Category/Top/OpenNhds.lean
feat: port Topology.Category.Top.OpenNhds (#3834)
Added TopologicalSpace.OpenNhds.infLeLeftView on Github →