# 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 →