Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-07 17:24 f519a125

View on Github →

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

Estimated changes

Modified src/topology/constructions.lean

deleted theorem list.continuous_at_length

deleted theorem list.continuous_insert_nth

deleted theorem list.continuous_remove_nth

deleted theorem list.tendsto_cons'

deleted theorem list.tendsto_cons

deleted theorem list.tendsto_cons_iff

deleted theorem list.tendsto_insert_nth'

deleted theorem list.tendsto_insert_nth

deleted theorem list.tendsto_nhds

deleted theorem list.tendsto_remove_nth

deleted theorem vector.cons_val

deleted theorem vector.continuous_at_remove_nth

deleted theorem vector.continuous_insert_nth'

deleted theorem vector.continuous_insert_nth

deleted theorem vector.continuous_remove_nth

deleted theorem vector.tendsto_cons

deleted theorem vector.tendsto_insert_nth

Created src/topology/list.lean

added theorem list.continuous_at_length

added theorem list.continuous_insert_nth

added theorem list.continuous_remove_nth

added theorem list.tendsto_cons'

added theorem list.tendsto_cons

added theorem list.tendsto_cons_iff

added theorem list.tendsto_insert_nth'

added theorem list.tendsto_insert_nth

added theorem list.tendsto_nhds

added theorem list.tendsto_remove_nth

added theorem nhds_cons

added theorem nhds_list

added theorem nhds_nil

added theorem vector.cons_val

added theorem vector.continuous_at_remove_nth

added theorem vector.continuous_insert_nth'

added theorem vector.continuous_insert_nth

added theorem vector.continuous_remove_nth

added theorem vector.tendsto_cons

added theorem vector.tendsto_insert_nth

Modified src/topology/order.lean

deleted theorem nhds_cons

deleted theorem nhds_list

deleted theorem nhds_nil