Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-23 14:24 4018daff

View on Github →

feat(topology): sequences, sequential spaces, and sequential continuity (closes #440) Co-Authored-By: Reid Barton rwbarton@gmail.com

Estimated changes

Created src/topology/sequences.lean

added theorem sequence.const_seq_conv

added theorem sequence.cont_iff_seq_cont

added theorem sequence.cont_to_seq_cont

added theorem sequence.is_mem_of_conv_to_of_is_seq_closed

added theorem sequence.is_mem_of_is_closed_of_conv_to

added def sequence.is_seq_closed

added theorem sequence.is_seq_closed_iff_is_closed

added theorem sequence.is_seq_closed_of_def

added theorem sequence.is_seq_closed_of_is_closed

added theorem sequence.metric_space.seq_tendsto_iff

added def sequence.sequential_closure

added theorem sequence.sequential_closure_subset_closure

added def sequence.sequentially_continuous

added theorem sequence.subset_seq_closure

added theorem sequence.topological_space.seq_tendsto_iff