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 →