Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-27 08:24 7e0b994c

View on Github →

feat(topology/compact_convergence): define compact convergence (#10967) And prove that the topology it induces is the compact-open topology

Estimated changes

Modified src/topology/compact_open.lean

Modified src/topology/order.lean

added theorem topological_space.nhds_mk_of_nhds_filter_basis

Created src/topology/uniform_space/compact_convergence.lean

added theorem continuous_map.Inter_compact_open_gen_subset_compact_conv_nhd

added def continuous_map.compact_conv_nhd

added theorem continuous_map.compact_conv_nhd_compact_entourage_nonempty

added theorem continuous_map.compact_conv_nhd_filter_is_basis

added theorem continuous_map.compact_conv_nhd_mem_comp

added theorem continuous_map.compact_conv_nhd_mono

added theorem continuous_map.compact_conv_nhd_nhd_basis

added theorem continuous_map.compact_conv_nhd_subset_compact_open

added theorem continuous_map.compact_conv_nhd_subset_inter

added def continuous_map.compact_convergence_filter_basis

added def continuous_map.compact_convergence_topology

added def continuous_map.compact_convergence_uniformity

added theorem continuous_map.compact_open_eq_compact_convergence

added theorem continuous_map.has_basis_compact_convergence_uniformity

added theorem continuous_map.has_basis_nhds_compact_convergence

added theorem continuous_map.mem_compact_convergence_entourage_iff

added theorem continuous_map.mem_compact_convergence_nhd_filter

added theorem continuous_map.mem_compact_convergence_uniformity

added theorem continuous_map.nhds_compact_convergence

added theorem continuous_map.self_mem_compact_conv_nhd

added theorem continuous_map.tendsto_iff_forall_compact_tendsto_uniformly_on'

added theorem continuous_map.tendsto_iff_forall_compact_tendsto_uniformly_on