Commit 2023-02-14 18:21 0f5ac2f7

View on Github →

feat: port Topology.UniformSpace.CompactConvergence (#2281)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UniformSpace/CompactConvergence.lean

added def ContinuousMap.compactConvNhd

added theorem ContinuousMap.compactConvNhd_compact_entourage_nonempty

added theorem ContinuousMap.compactConvNhd_filter_isBasis

added theorem ContinuousMap.compactConvNhd_mem_comp

added theorem ContinuousMap.compactConvNhd_mono

added theorem ContinuousMap.compactConvNhd_nhd_basis

added theorem ContinuousMap.compactConvNhd_subset_compactOpen

added theorem ContinuousMap.compactConvNhd_subset_inter

added def ContinuousMap.compactConvergenceFilterBasis

added def ContinuousMap.compactConvergenceTopology

added def ContinuousMap.compactConvergenceUniformity

added theorem ContinuousMap.compactOpen_eq_compactConvergence

added theorem ContinuousMap.hasBasis_compactConvergenceUniformity

added theorem ContinuousMap.hasBasis_compactConvergenceUniformity_aux

added theorem ContinuousMap.hasBasis_compactConvergenceUniformity_of_compact

added theorem ContinuousMap.hasBasis_nhds_compactConvergence

added theorem ContinuousMap.interᵢ_compactOpen_gen_subset_compactConvNhd

added theorem ContinuousMap.mem_compactConvergenceUniformity

added theorem ContinuousMap.mem_compactConvergence_entourage_iff

added theorem ContinuousMap.mem_compactConvergence_nhd_filter

added theorem ContinuousMap.nhds_compactConvergence

added theorem ContinuousMap.self_mem_compactConvNhd

added theorem ContinuousMap.tendstoLocallyUniformly_of_tendsto

added theorem ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn'

added theorem ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn

added theorem ContinuousMap.tendsto_iff_tendstoLocallyUniformly

added theorem ContinuousMap.tendsto_iff_tendstoUniformly

added theorem ContinuousMap.tendsto_of_tendstoLocallyUniformly

added theorem Filter.HasBasis.compactConvergenceUniformity