Commit 2023-02-04 18:05 1f80678a

View on Github →

feat: port Topology.UniformSpace.UniformConvergence (#2051)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Filter/Prod.lean

added theorem Filter.inf_prod

added theorem Filter.mem_prod_iff_left

added theorem Filter.mem_prod_iff_right

added theorem Filter.prod_inf

added theorem Filter.prod_map_left

added theorem Filter.prod_map_right

Modified Mathlib/Topology/ContinuousOn.lean

added theorem nhdsWithin_eq_nhds

Created Mathlib/Topology/UniformSpace/UniformConvergence.lean

added theorem Filter.Tendsto.tendstoUniformlyOnFilter_const

added theorem Filter.Tendsto.tendstoUniformlyOn_const

added theorem TendstoLocallyUniformly.comp

added theorem TendstoLocallyUniformly.tendsto_comp

added def TendstoLocallyUniformly

added theorem TendstoLocallyUniformlyOn.comp

added theorem TendstoLocallyUniformlyOn.congr

added theorem TendstoLocallyUniformlyOn.congr_right

added theorem TendstoLocallyUniformlyOn.mono

added theorem TendstoLocallyUniformlyOn.tendsto_at

added theorem TendstoLocallyUniformlyOn.tendsto_comp

added theorem TendstoLocallyUniformlyOn.union

added theorem TendstoLocallyUniformlyOn.unique

added def TendstoLocallyUniformlyOn

added theorem TendstoUniformly.comp

added theorem TendstoUniformly.prod

added theorem TendstoUniformly.prod_map

added theorem TendstoUniformly.tendstoUniformlyOnFilter

added theorem TendstoUniformly.tendsto_at

added theorem TendstoUniformly.tendsto_comp

added def TendstoUniformly

added theorem TendstoUniformlyOn.comp

added theorem TendstoUniformlyOn.congr

added theorem TendstoUniformlyOn.congr_right

added theorem TendstoUniformlyOn.mono

added theorem TendstoUniformlyOn.prod

added theorem TendstoUniformlyOn.prod_map

added theorem TendstoUniformlyOn.seq_tendstoUniformlyOn

added theorem TendstoUniformlyOn.tendsto_at

added theorem TendstoUniformlyOn.tendsto_comp

added theorem TendstoUniformlyOn.uniformCauchySeqOn

added def TendstoUniformlyOn

added theorem TendstoUniformlyOnFilter.comp

added theorem TendstoUniformlyOnFilter.congr

added theorem TendstoUniformlyOnFilter.mono_left

added theorem TendstoUniformlyOnFilter.mono_right

added theorem TendstoUniformlyOnFilter.prod

added theorem TendstoUniformlyOnFilter.prod_map

added theorem TendstoUniformlyOnFilter.tendsto_at

added theorem TendstoUniformlyOnFilter.uniformCauchySeqOnFilter

added def TendstoUniformlyOnFilter

added theorem UniformCauchySeqOn.cauchy_map

added theorem UniformCauchySeqOn.comp

added theorem UniformCauchySeqOn.mono

added theorem UniformCauchySeqOn.prod'

added theorem UniformCauchySeqOn.prod

added theorem UniformCauchySeqOn.prod_map

added theorem UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto

added theorem UniformCauchySeqOn.uniformCauchySeqOnFilter

added def UniformCauchySeqOn

added theorem UniformCauchySeqOnFilter.comp

added theorem UniformCauchySeqOnFilter.mono_left

added theorem UniformCauchySeqOnFilter.mono_right

added theorem UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto

added def UniformCauchySeqOnFilter

added theorem UniformContinuous.comp_tendstoUniformly

added theorem UniformContinuous.comp_tendstoUniformlyOn

added theorem UniformContinuous.comp_tendstoUniformlyOnFilter

added theorem UniformContinuous.comp_uniformCauchySeqOn

added theorem UniformContinuousOn.tendstoUniformly

added theorem UniformContinuousOn.tendstoUniformlyOn

added theorem UniformContinuous₂.tendstoUniformly

added theorem continuousAt_of_locally_uniform_approx_of_continuousAt

added theorem continuousOn_of_locally_uniform_approx_of_continuousWithinAt

added theorem continuousOn_of_uniform_approx_of_continuousOn

added theorem continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt

added theorem continuous_of_locally_uniform_approx_of_continuousAt

added theorem continuous_of_uniform_approx_of_continuous

added theorem tendstoLocallyUniformlyOn_TFAE

added theorem tendstoLocallyUniformlyOn_bunionᵢ

added theorem tendstoLocallyUniformlyOn_iff_filter

added theorem tendstoLocallyUniformlyOn_iff_forall_isCompact

added theorem tendstoLocallyUniformlyOn_iff_forall_tendsto

added theorem tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe

added theorem tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact

added theorem tendstoLocallyUniformlyOn_unionᵢ

added theorem tendstoLocallyUniformlyOn_unionₛ

added theorem tendstoLocallyUniformlyOn_univ

added theorem tendstoLocallyUniformly_iff_filter

added theorem tendstoLocallyUniformly_iff_forall_tendsto

added theorem tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace

added theorem tendstoUniformlyOnFilter_iff_tendsto

added theorem tendstoUniformlyOn_empty

added theorem tendstoUniformlyOn_iff_seq_tendstoUniformlyOn

added theorem tendstoUniformlyOn_iff_tendsto

added theorem tendstoUniformlyOn_iff_tendstoUniformlyOnFilter

added theorem tendstoUniformlyOn_iff_tendstoUniformly_comp_coe

added theorem tendstoUniformlyOn_of_seq_tendstoUniformlyOn

added theorem tendstoUniformlyOn_singleton_iff_tendsto

added theorem tendstoUniformlyOn_univ

added theorem tendstoUniformly_iff_seq_tendstoUniformly

added theorem tendstoUniformly_iff_tendsto

added theorem tendstoUniformly_iff_tendstoUniformlyOnFilter

added theorem tendsto_comp_of_locally_uniform_limit

added theorem tendsto_comp_of_locally_uniform_limit_within

added theorem tendsto_prod_filter_iff

added theorem tendsto_prod_principal_iff

added theorem tendsto_prod_top_iff

added theorem uniformCauchySeqOn_iff_uniformCauchySeqOnFilter