Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-23 14:24 9be8905e

View on Github →

refactor(topology/sequences): restructure proofs

Estimated changes

Modified src/topology/sequences.lean

added theorem continuous.to_sequentially_continuous

added theorem continuous_iff_sequentially_continuous

added def is_seq_closed

added theorem is_seq_closed_iff_is_closed

added theorem is_seq_closed_of_def

added theorem is_seq_closed_of_is_closed

added theorem mem_of_is_closed_sequential

added theorem mem_of_is_seq_closed

deleted theorem sequence.const_seq_conv

deleted theorem sequence.cont_iff_seq_cont

deleted theorem sequence.cont_to_seq_cont

deleted theorem sequence.is_mem_of_conv_to_of_is_seq_closed

deleted theorem sequence.is_mem_of_is_closed_of_conv_to

deleted def sequence.is_seq_closed

deleted theorem sequence.is_seq_closed_iff_is_closed

deleted theorem sequence.is_seq_closed_of_def

deleted theorem sequence.is_seq_closed_of_is_closed

deleted theorem sequence.metric_space.seq_tendsto_iff

deleted def sequence.sequential_closure

deleted theorem sequence.sequential_closure_subset_closure

deleted def sequence.sequentially_continuous

deleted theorem sequence.subset_seq_closure

deleted theorem sequence.topological_space.seq_tendsto_iff

added def sequential_closure

added theorem sequential_closure_subset_closure

added def sequentially_continuous

added theorem subset_sequential_closure

added theorem topological_space.seq_tendsto_iff