Commit 2023-02-03 08:41 a5cca0f0

View on Github →

feat: port Topology.UniformSpace.Cauchy (#2007)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Logic/Equiv/Basic.lean

Created Mathlib/Topology/UniformSpace/Cauchy.lean

added theorem Cauchy.comap'

added theorem Cauchy.le_nhds_lim

added theorem Cauchy.mono'

added theorem Cauchy.mono

added theorem Cauchy.prod

added theorem Cauchy.ultrafilter_of

added def Cauchy

added theorem CauchySeq.comp_injective

added theorem CauchySeq.comp_tendsto

added theorem CauchySeq.eventually_eventually

added theorem CauchySeq.mem_entourage

added theorem CauchySeq.nonempty

added theorem CauchySeq.prod

added theorem CauchySeq.prod_map

added theorem CauchySeq.subseq_mem

added theorem CauchySeq.subseq_subseq_mem

added theorem CauchySeq.tendsto_limUnder

added theorem CauchySeq.tendsto_uniformity

added theorem CauchySeq.totallyBounded_range

added def CauchySeq

added theorem Filter.HasBasis.cauchySeq_iff'

added theorem Filter.HasBasis.cauchySeq_iff

added theorem Filter.HasBasis.cauchy_iff

added theorem Filter.HasBasis.totallyBounded_iff

added theorem Filter.Tendsto.cauchySeq

added theorem Filter.Tendsto.cauchy_map

added theorem Filter.Tendsto.subseq_mem_entourage

added theorem Function.Bijective.cauchySeq_comp_iff

added theorem IsClosed.isComplete

added def IsComplete

added theorem SequentiallyComplete.le_nhds_of_seq_tendsto_nhds

added def SequentiallyComplete.seq

added theorem SequentiallyComplete.seq_is_cauchySeq

added theorem SequentiallyComplete.seq_mem

added theorem SequentiallyComplete.seq_pair_mem

added def SequentiallyComplete.setSeq

added def SequentiallyComplete.setSeqAux

added theorem SequentiallyComplete.setSeq_mem

added theorem SequentiallyComplete.setSeq_mono

added theorem SequentiallyComplete.setSeq_prod_subset

added theorem SequentiallyComplete.setSeq_sub_aux

added theorem TotallyBounded.closure

added theorem TotallyBounded.exists_subset

added theorem TotallyBounded.image

added def TotallyBounded

added theorem Ultrafilter.cauchy_of_totallyBounded

added theorem UniformContinuous.comp_cauchySeq

added theorem UniformSpace.complete_of_cauchySeq_tendsto

added theorem UniformSpace.complete_of_convergent_controlled_sequences

added theorem UniformSpace.second_countable_of_separable

added theorem cauchySeq_const

added theorem cauchySeq_iff'

added theorem cauchySeq_iff

added theorem cauchySeq_iff_tendsto

added theorem cauchySeq_of_controlled

added theorem cauchySeq_tendsto_of_complete

added theorem cauchySeq_tendsto_of_isComplete

added theorem cauchy_iff'

added theorem cauchy_iff

added theorem cauchy_iff_exists_le_nhds

added theorem cauchy_map_iff'

added theorem cauchy_map_iff

added theorem cauchy_map_iff_exists_tendsto

added theorem cauchy_nhds

added theorem cauchy_pure

added theorem completeSpace_iff_isComplete_univ

added theorem completeSpace_iff_ultrafilter

added theorem completeSpace_of_isComplete_univ

added theorem complete_univ

added theorem isCompact_iff_totallyBounded_isComplete

added theorem isCompact_of_totallyBounded_isClosed

added theorem isComplete_iff_clusterPt

added theorem isComplete_iff_ultrafilter'

added theorem isComplete_iff_ultrafilter

added theorem isComplete_unionᵢ_separated

added theorem le_nhds_iff_adhp_of_cauchy

added theorem le_nhds_of_cauchy_adhp

added theorem le_nhds_of_cauchy_adhp_aux

added theorem tendsto_nhds_of_cauchySeq_of_subseq

added theorem totallyBounded_empty

added theorem totallyBounded_iff_filter

added theorem totallyBounded_iff_subset

added theorem totallyBounded_iff_ultrafilter

added theorem totallyBounded_of_forall_symm

added theorem totallyBounded_subset