Commit 2024-02-25 01:09 a36350f2

View on Github →

refactor(UniformConvergenceTopology): redefine using UniformOnFun (#10873)

Estimated changes

Modified Mathlib/Topology/CompactOpen.lean

added theorem ContinuousMap.nhds_compactOpen

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean

deleted def ContinuousMap.compactConvNhd

deleted theorem ContinuousMap.compactConvNhd_compact_entourage_nonempty

deleted theorem ContinuousMap.compactConvNhd_filter_isBasis

deleted theorem ContinuousMap.compactConvNhd_mem_comp

deleted theorem ContinuousMap.compactConvNhd_mono

deleted theorem ContinuousMap.compactConvNhd_nhd_basis

deleted theorem ContinuousMap.compactConvNhd_subset_compactOpen

deleted theorem ContinuousMap.compactConvNhd_subset_inter

deleted def ContinuousMap.compactConvergenceFilterBasis

deleted def ContinuousMap.compactConvergenceTopology

deleted def ContinuousMap.compactConvergenceUniformity

deleted theorem ContinuousMap.compactOpen_eq_compactConvergence

deleted theorem ContinuousMap.hasBasis_compactConvergenceUniformity_aux

deleted theorem ContinuousMap.hasBasis_nhds_compactConvergence

deleted theorem ContinuousMap.iInter_compactOpen_gen_subset_compactConvNhd

deleted theorem ContinuousMap.mem_compactConvergenceUniformity

deleted theorem ContinuousMap.mem_compactConvergence_nhd_filter

deleted theorem ContinuousMap.nhds_compactConvergence

deleted theorem ContinuousMap.self_mem_compactConvNhd

deleted theorem ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn'

modified theorem ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn

added def ContinuousMap.toUniformOnFunIsCompact

added theorem ContinuousMap.toUniformOnFun_toFun

added theorem ContinuousMap.uniformEmbedding_toUniformOnFunIsCompact