Theorem Topology.IsUpper.isTopologicalBasis_insert_univ_subbasis

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.IsUpper.isTopologicalBasis_insert_univ_subbasisView on Github →