Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-19 00:14 ed842981

View on Github →

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

Estimated changes

Modified analysis/topology/continuity.lean

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_length

added theorem list.tendsto_nhds

added theorem list.tendsto_remove_nth

added theorem tendsto_subtype_rng

added theorem tendsto_subtype_val

added theorem vector.cons_val

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

added theorem vector.tendsto_remove_nth

Modified analysis/topology/topological_space.lean

added theorem nhds_cons

added theorem nhds_nil

Modified analysis/topology/uniform_space.lean