Theorem isClosed_and_discrete_iff

Modification history

2023-10-11 21:40

Mathlib/Topology/Compactness/Compact.lean

chore(Topology/SubsetProperties): Refactor SubsetProperties.lean (#7628) …

Modified isClosed_and_discrete_iff View on Github →

2023-10-09 21:43

Mathlib/Topology/SubsetProperties.lean

feat(Topology/Separation): filter of codiscrete sets (#7456) …

Added isClosed_and_discrete_iff View on Github →