Theorem Topology.IsLower.isTopologicalSpace_basis

Modification history

2024-08-16 13:44
Mathlib/Topology/Order/LowerUpperTopology.lean
feat(Topology/Order/LowerUpperTopology): Scott and Upper topologies coincide on a complete linear order (#12234) …
Added Topology.IsLower.isTopologicalSpace_basisView on Github →