Mathlib v3 is deprecated. Go to Mathlib v4

Theorem list.continuous_insert_nth

Modification history

2019-10-07 17:24

src/topology/constructions.lean

refactor(topology/list): move topology of lists, vectors to new file (#1514)

Modified list.continuous_insert_nth View on Github →

2018-10-19 00:14

analysis/topology/continuity.lean

feat(analysis/topology): add continuity rules for list and vector insert/remove_nth

Added list.continuous_insert_nth View on Github →