Commit 2023-02-16 01:18 aeba7cb8

View on Github →

feat: Port/Topology.List (#2287) port of topology.list

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/List.lean

added theorem Filter.Tendsto.cons

added theorem List.continuousAt_length

added theorem List.continuous_cons

added theorem List.continuous_insertNth

added theorem List.continuous_prod

added theorem List.continuous_removeNth

added theorem List.tendsto_cons

added theorem List.tendsto_cons_iff

added theorem List.tendsto_insertNth

added theorem List.tendsto_insert_nth'

added theorem List.tendsto_nhds

added theorem List.tendsto_prod

added theorem List.tendsto_removeNth

added theorem Vector.continuousAt_removeNth

added theorem Vector.continuous_insertNth

added theorem Vector.continuous_insert_nth'

added theorem Vector.continuous_removeNth

added theorem Vector.tendsto_cons

added theorem Vector.tendsto_insertNth

added theorem nhds_cons

added theorem nhds_list

added theorem nhds_nil