Mathlib v3 is deprecated. Go to Mathlib v4

Theorem t2_separation

Modification history

2019-03-03 19:05

src/topology/basic.lean

chore(topology): Splits topology.basic and topology.continuity (#785) …

Modified t2_separation View on Github →

2017-08-27 12:26

topology/topological_space.lean

fix(.): adapt to Lean changes: type class parameters to structures are now type class parameters in the projections and constructor

Modified t2_separation View on Github →

2017-08-10 16:36

topology/topological_space.lean

construct reals as complete, linear ordered field

Added t2_separation View on Github →