Commit 2023-05-30 04:33 15f033db

View on Github →

feat: port Topology.Instances.Discrete (#4479)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Instances/Discrete.lean

added theorem LinearOrder.bot_topologicalSpace_eq_generateFrom

added theorem bot_topologicalSpace_eq_generateFrom_of_pred_succOrder

added theorem discreteTopology_iff_orderTopology_of_pred_succ'

added theorem discreteTopology_iff_orderTopology_of_pred_succ