Def continuous

Modification history

2020-11-18 21:10
src/topology/basic.lean
refactor(*): make continuous a structure (#5035) …
Deleted continuousView on Github →
2019-03-03 19:05
src/topology/basic.lean
chore(topology): Splits topology.basic and topology.continuity (#785) …
Modified continuousView on Github →
2018-01-11 23:22
analysis/topology/continuity.lean
doc(*): blurbs galore …
Modified continuousView on Github →
2017-08-10 16:41
topology/continuity.lean
rename open -> is_open, closed -> is_closed
Modified continuousView on Github →
2017-08-02 22:32
topology/continuity.lean
refactor(data/set/basic,*): vimage -> preimage, add notation
Modified continuousView on Github →
2017-07-23 15:16
topology/continuity.lean
refactor(*): import content from lean/library/data and library_dev
Added continuousView on Github →