Commit 2023-07-10 12:17 ea5be102

View on Github →

feat: add lemmas about discrete topology (#5777)

Use section variables.
Add closure_discrete, dense_discrete, denseRange_discrete, and discreteTopology_iff_forall_isClosed.

Estimated changes

Modified Mathlib/Topology/Order.lean

added theorem closure_discrete

modified theorem continuous_of_discreteTopology

added theorem denseRange_discrete

added theorem dense_discrete

added theorem discreteTopology_iff_forall_isClosed

modified theorem isClosed_discrete

modified theorem isOpen_discrete

modified theorem mem_nhds_discrete