Commit 2023-03-03 21:38 28c23e3c

View on Github →

feat: port Topology.Sequences (#2604)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Order.lean

modified theorem continuous_Prop

modified theorem isOpen_iff_continuous_mem

added theorem tendsto_nhds_Prop

added theorem tendsto_nhds_true

Created Mathlib/Topology/Sequences.lean

added theorem CompactSpace.tendsto_subseq

added theorem FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto

added theorem IsCompact.tendsto_subseq'

added theorem IsCompact.tendsto_subseq

added theorem IsSeqClosed.preimage

added theorem IsSeqClosed.seqClosure_eq

added def IsSeqClosed

added theorem IsSeqCompact.exists_tendsto

added theorem IsSeqCompact.exists_tendsto_of_frequently_mem

added theorem IsSeqCompact.subseq_of_frequently_in

added def IsSeqCompact

added theorem QuotientMap.sequentialSpace

added theorem SeqCompactSpace.tendsto_subseq

added def SeqContinuous

added theorem UniformSpace.compactSpace_iff_seqCompactSpace

added theorem continuous_iff_seqContinuous

added theorem isSeqClosed_iff

added theorem isSeqClosed_iff_isClosed

added theorem isSeqClosed_of_seqClosure_eq

added theorem mem_closure_iff_seq_limit

added def seqClosure

added theorem seqClosure_eq_closure

added theorem seqClosure_subset_closure

added theorem subset_seqClosure

added theorem tendsto_nhds_iff_seq_tendsto

added theorem tendsto_subseq_of_bounded

added theorem tendsto_subseq_of_frequently_bounded