Documentation Verification Report

UniformConvergence

📁 Source: Mathlib/Topology/UniformSpace/UniformConvergence.lean

Statistics

Metric	Count
Definitions `TendstoUniformly`, `TendstoUniformlyOn`, `TendstoUniformlyOnFilter`, `UniformCauchySeqOn`, `UniformCauchySeqOnFilter`	5
Theorems `tendstoUniformlyOnFilter_iff`, `tendstoUniformlyOnFilter_iff_of_uniformity`, `tendstoUniformlyOn_iff`, `tendstoUniformlyOn_iff_of_uniformity`, `tendstoUniformly_iff`, `tendstoUniformly_iff_of_uniformity`, `tendstoUniformlyOnFilter_const`, `tendstoUniformlyOn_const`, `comp`, `prodMap`, `prodMk`, `tendstoUniformlyOn`, `tendstoUniformlyOnFilter`, `tendsto_at`, `tendsto_of_eventually_tendsto`, `comp`, `congr_inseparable`, `congr_inseparable_right`, `congr_right`, `mono`, `prodMap`, `prodMk`, `seq_tendstoUniformlyOn`, `tendstoUniformlyOnFilter`, `tendsto_at`, `uniformCauchySeqOn`, `comp`, `congr_inseparable`, `mono_left`, `mono_right`, `prodMap`, `prodMk`, `tendstoUniformlyOn`, `tendsto_at`, `tendsto_of_eventually_tendsto`, `uniformCauchySeqOnFilter`, `cauchySeq`, `cauchy_map`, `comp`, `mono`, `prod`, `prod'`, `prodMap`, `tendstoUniformlyOn_of_tendsto`, `uniformCauchySeqOnFilter`, `comp`, `mono_left`, `mono_right`, `tendstoUniformlyOnFilter_of_tendsto`, `comp_tendstoUniformly`, `comp_tendstoUniformlyOn`, `comp_tendstoUniformlyOnFilter`, `comp_uniformCauchySeqOn`, `tendstoUniformly`, `tendstoUniformlyOn`, `tendstoUniformly`, `tendstoUniformlyOnFilter_iff_tendsto`, `tendstoUniformlyOn_empty`, `tendstoUniformlyOn_iff_restrict`, `tendstoUniformlyOn_iff_seq_tendstoUniformlyOn`, `tendstoUniformlyOn_iff_tendsto`, `tendstoUniformlyOn_iff_tendstoUniformlyOnFilter`, `tendstoUniformlyOn_iff_tendstoUniformly_comp_coe`, `tendstoUniformlyOn_of_seq_tendstoUniformlyOn`, `tendstoUniformlyOn_singleton_iff_tendsto`, `tendstoUniformlyOn_univ`, `tendstoUniformly_congr`, `tendstoUniformly_congr_inseparable`, `tendstoUniformly_iff_seq_tendstoUniformly`, `tendstoUniformly_iff_tendsto`, `tendstoUniformly_iff_tendstoUniformlyOnFilter`, `tendsto_prod_filter_iff`, `tendsto_prod_principal_iff`, `tendsto_prod_top_iff`, `uniformCauchySeqOn_iff_uniformCauchySeqOnFilter`	75
Total	80

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoUniformlyOnFilter_iff` 📖	mathematical	`Filter.HasBasis` `uniformity`	`TendstoUniformlyOnFilter` `Set` `Set.instMembership`	—	`tendstoUniformlyOnFilter_iff_of_uniformity` `eventually_iff` `prod`
`tendstoUniformlyOnFilter_iff_of_uniformity` 📖	mathematical	`Filter.HasBasis` `uniformity`	`TendstoUniformlyOnFilter` `Filter.Eventually` `Set` `Set.instMembership` `SProd.sprod` `Filter` `Filter.instSProd`	—	`tendstoUniformlyOnFilter_iff_tendsto` `tendsto_right_iff`
`tendstoUniformlyOn_iff` 📖	mathematical	`Filter.HasBasis` `uniformity`	`TendstoUniformlyOn` `Set` `Set.instMembership`	—	`tendstoUniformlyOn_iff_of_uniformity` `eventually_iff`
`tendstoUniformlyOn_iff_of_uniformity` 📖	mathematical	`Filter.HasBasis` `uniformity`	`TendstoUniformlyOn` `Filter.Eventually`	—	`tendsto_right_iff`
`tendstoUniformly_iff` 📖	mathematical	`Filter.HasBasis` `uniformity`	`TendstoUniformly` `Set` `Set.instMembership`	—	`tendstoUniformly_iff_of_uniformity` `eventually_iff`
`tendstoUniformly_iff_of_uniformity` 📖	mathematical	`Filter.HasBasis` `uniformity`	`TendstoUniformly` `Filter.Eventually`	—	`tendstoUniformlyOn_iff_of_uniformity`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoUniformlyOnFilter_const` 📖	mathematical	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	`TendstoUniformlyOnFilter`	—	`nhds_eq_comap_uniformity` `comp` `Filter.tendsto_fst`
`tendstoUniformlyOn_const` 📖	mathematical	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	`TendstoUniformlyOn`	—	`tendstoUniformlyOn_iff_tendstoUniformlyOnFilter` `tendstoUniformlyOnFilter_const`

TendstoUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`TendstoUniformly`	`TendstoUniformly`	—	`tendstoUniformly_iff_tendstoUniformlyOnFilter` `Filter.comap_top` `TendstoUniformlyOnFilter.comp`
`prodMap` 📖	mathematical	`TendstoUniformly`	`TendstoUniformly` `instUniformSpaceProd` `SProd.sprod` `Filter` `Filter.instSProd`	—	`tendstoUniformlyOn_univ` `Set.univ_prod_univ` `TendstoUniformlyOn.prodMap`
`prodMk` 📖	mathematical	`TendstoUniformly`	`TendstoUniformly` `instUniformSpaceProd` `SProd.sprod` `Filter` `Filter.instSProd`	—	`comp` `prodMap`
`tendstoUniformlyOn` 📖	mathematical	`TendstoUniformly`	`TendstoUniformlyOn`	—	`TendstoUniformlyOn.mono` `tendstoUniformlyOn_univ` `Set.subset_univ`
`tendstoUniformlyOnFilter` 📖	mathematical	`TendstoUniformly`	`TendstoUniformlyOnFilter` `Top.top` `Filter` `Filter.instTop`	—	`tendstoUniformly_iff_tendstoUniformlyOnFilter`
`tendsto_at` 📖	mathematical	`TendstoUniformly`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	—	`TendstoUniformlyOnFilter.tendsto_at` `tendstoUniformlyOnFilter` `le_top`
`tendsto_of_eventually_tendsto` 📖	mathematical	`TendstoUniformly` `Filter.Eventually` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	—	`TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto` `TendstoUniformlyOnFilter.mono_right` `tendstoUniformlyOnFilter` `le_top`

TendstoUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`TendstoUniformlyOn`	`TendstoUniformlyOn` `Set.preimage`	—	`tendstoUniformlyOn_iff_tendstoUniformlyOnFilter` `Filter.comap_principal` `TendstoUniformlyOnFilter.comp`
`congr_inseparable` 📖	mathematical	`TendstoUniformlyOn` `Filter.Eventually`	`TendstoUniformlyOn`	—	`tendstoUniformlyOn_iff_tendstoUniformlyOnFilter` `TendstoUniformlyOnFilter.congr_inseparable` `Filter.eventually_prod_principal_iff`
`congr_inseparable_right` 📖	mathematical	`TendstoUniformlyOn` `Inseparable` `UniformSpace.toTopologicalSpace`	`TendstoUniformlyOn`	—	`tendstoUniformlyOn_iff_tendsto` `Filter.HasBasis.tendsto_right_iff` `uniformity_hasBasis_open` `forall₂_imp` `Filter.eventually_prod_principal_iff` `Filter.Eventually.mono` `Inseparable.mem_open_iff` `Inseparable.prod` `Inseparable.rfl`
`congr_right` 📖	mathematical	`TendstoUniformlyOn` `Set.EqOn`	`TendstoUniformlyOn`	—	`congr_inseparable_right` `Inseparable.of_eq`
`mono` 📖	mathematical	`TendstoUniformlyOn` `Set` `Set.instHasSubset`	`TendstoUniformlyOn`	—	`tendstoUniformlyOn_iff_tendstoUniformlyOnFilter` `TendstoUniformlyOnFilter.mono_right` `tendstoUniformlyOnFilter` `Filter.le_principal_iff` `Filter.mem_principal`
`prodMap` 📖	mathematical	`TendstoUniformlyOn`	`TendstoUniformlyOn` `instUniformSpaceProd` `SProd.sprod` `Filter` `Filter.instSProd` `Set` `Set.instSProd`	—	`tendstoUniformlyOn_iff_tendstoUniformlyOnFilter` `Filter.prod_principal_principal` `TendstoUniformlyOnFilter.prodMap`
`prodMk` 📖	mathematical	`TendstoUniformlyOn`	`TendstoUniformlyOn` `instUniformSpaceProd` `SProd.sprod` `Filter` `Filter.instSProd`	—	`Set.inter_self` `comp` `prodMap`
`seq_tendstoUniformlyOn` 📖	mathematical	`TendstoUniformlyOn` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder`	`TendstoUniformlyOn` `Filter.atTop` `Nat.instPreorder`	—	`tendstoUniformlyOn_iff_tendsto` `Filter.Tendsto.comp` `Filter.Tendsto.prodMk` `Filter.tendsto_fst` `Filter.tendsto_snd`
`tendstoUniformlyOnFilter` 📖	mathematical	`TendstoUniformlyOn`	`TendstoUniformlyOnFilter` `Filter.principal`	—	`tendstoUniformlyOn_iff_tendstoUniformlyOnFilter`
`tendsto_at` 📖	mathematical	`TendstoUniformlyOn` `Set` `Set.instMembership`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	—	`TendstoUniformlyOnFilter.tendsto_at` `tendstoUniformlyOnFilter` `Filter.le_principal_iff` `Filter.mem_principal` `Set.singleton_subset_iff`
`uniformCauchySeqOn` 📖	mathematical	`TendstoUniformlyOn`	`UniformCauchySeqOn`	—	`uniformCauchySeqOn_iff_uniformCauchySeqOnFilter` `TendstoUniformlyOnFilter.uniformCauchySeqOnFilter` `tendstoUniformlyOnFilter`

TendstoUniformlyOnFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`TendstoUniformlyOnFilter`	`TendstoUniformlyOnFilter` `Filter.comap`	—	`tendstoUniformlyOnFilter_iff_tendsto` `Filter.Tendsto.comp` `Filter.Tendsto.prodMap` `Filter.tendsto_id` `Filter.tendsto_comap`
`congr_inseparable` 📖	mathematical	`TendstoUniformlyOnFilter` `Filter.Eventually` `Inseparable` `UniformSpace.toTopologicalSpace` `SProd.sprod` `Filter` `Filter.instSProd`	`TendstoUniformlyOnFilter`	—	`tendstoUniformlyOnFilter_iff_tendsto` `Filter.HasBasis.tendsto_right_iff` `uniformity_hasBasis_open` `Filter.Eventually.congr` `Filter.Eventually.mono` `Inseparable.mem_open_iff` `Inseparable.prod` `Inseparable.rfl`
`mono_left` 📖	mathematical	`TendstoUniformlyOnFilter` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`TendstoUniformlyOnFilter`	—	`Filter.Eventually.filter_mono` `Filter.prod_mono_left`
`mono_right` 📖	mathematical	`TendstoUniformlyOnFilter` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`TendstoUniformlyOnFilter`	—	`Filter.Eventually.filter_mono` `Filter.prod_mono_right`
`prodMap` 📖	mathematical	`TendstoUniformlyOnFilter`	`TendstoUniformlyOnFilter` `instUniformSpaceProd` `SProd.sprod` `Filter` `Filter.instSProd`	—	`tendstoUniformlyOnFilter_iff_tendsto` `uniformity_prod_eq_comap_prod` `Filter.tendsto_comap_iff` `Filter.map_swap4_prod` `Filter.tendsto_map'_iff` `Filter.Tendsto.prodMap`
`prodMk` 📖	mathematical	`TendstoUniformlyOnFilter`	`TendstoUniformlyOnFilter` `instUniformSpaceProd` `SProd.sprod` `Filter` `Filter.instSProd`	—	`Filter.Eventually.diag_of_prod_right` `prodMap`
`tendstoUniformlyOn` 📖	mathematical	`TendstoUniformlyOnFilter` `Filter.principal`	`TendstoUniformlyOn`	—	`tendstoUniformlyOn_iff_tendstoUniformlyOnFilter`
`tendsto_at` 📖	mathematical	`TendstoUniformlyOnFilter` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal` `Set` `Set.instSingletonSet`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	—	`Uniform.tendsto_nhds_right` `Filter.mem_map` `Filter.mp_mem` `Filter.Eventually.curry` `Filter.univ_mem'` `Filter.principal_singleton` `Filter.Eventually.filter_mono`
`tendsto_of_eventually_tendsto` 📖	mathematical	`TendstoUniformlyOnFilter` `Filter.Eventually` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	—	`Uniform.tendsto_nhds_left` `Filter.mem_map` `Set.preimage.eq_1` `Filter.eventually_iff` `comp3_mem_uniformity` `Filter.mp_mem` `Filter.univ_mem'` `Filter.Eventually.curry` `Filter.Eventually.exists` `Filter.Eventually.and`
`uniformCauchySeqOnFilter` 📖	mathematical	`TendstoUniformlyOnFilter`	`UniformCauchySeqOnFilter`	—	`comp_symm_of_uniformity` `Filter.Tendsto.eventually` `Filter.tendsto_swap4_prod` `Filter.Eventually.mono` `Filter.Eventually.diag_of_prod_right` `SetRel.prodMk_mem_comp`

UniformCauchySeqOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchySeq` 📖	mathematical	`UniformCauchySeqOn` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Set` `Set.instMembership`	`CauchySeq` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`cauchy_map` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder`
`cauchy_map` 📖	mathematical	`UniformCauchySeqOn` `Set` `Set.instMembership`	`Cauchy` `Filter.map`	—	`Filter.mem_map` `Filter.mp_mem` `Filter.univ_mem'`
`comp` 📖	mathematical	`UniformCauchySeqOn`	`UniformCauchySeqOn` `Set.preimage`	—	`uniformCauchySeqOn_iff_uniformCauchySeqOnFilter` `Filter.comap_principal` `UniformCauchySeqOnFilter.comp`
`mono` 📖	mathematical	`UniformCauchySeqOn` `Set` `Set.instHasSubset`	`UniformCauchySeqOn`	—	`uniformCauchySeqOn_iff_uniformCauchySeqOnFilter` `UniformCauchySeqOnFilter.mono_right` `Filter.le_principal_iff` `Filter.mem_principal`
`prod` 📖	mathematical	`UniformCauchySeqOn`	`UniformCauchySeqOn` `instUniformSpaceProd` `SProd.sprod` `Filter` `Filter.instSProd`	—	`Set.inter_self` `comp` `prodMap`
`prod'` 📖	mathematical	`UniformCauchySeqOn`	`UniformCauchySeqOn` `instUniformSpaceProd`	—	`Filter.tendsto_diag` `Filter.Tendsto.eventually` `Filter.Tendsto.prodMap` `prod`
`prodMap` 📖	mathematical	`UniformCauchySeqOn`	`UniformCauchySeqOn` `instUniformSpaceProd` `SProd.sprod` `Filter` `Filter.instSProd` `Set` `Set.instSProd`	—	`Filter.mem_prod_iff` `Filter.mem_map` `uniformity_prod_eq_prod` `Filter.Eventually.mono` `Filter.Tendsto.eventually` `Filter.tendsto_swap4_prod` `Set.image_subset_iff` `Set.mk_mem_prod`
`tendstoUniformlyOn_of_tendsto` 📖	mathematical	`UniformCauchySeqOn` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	`TendstoUniformlyOn`	—	`tendstoUniformlyOn_iff_tendstoUniformlyOnFilter` `UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto` `uniformCauchySeqOnFilter`
`uniformCauchySeqOnFilter` 📖	mathematical	`UniformCauchySeqOn`	`UniformCauchySeqOnFilter` `Filter.principal`	—	`uniformCauchySeqOn_iff_uniformCauchySeqOnFilter`

UniformCauchySeqOnFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`UniformCauchySeqOnFilter`	`UniformCauchySeqOnFilter` `Filter.comap`	—	`Filter.eventually_prod_iff` `Filter.eventually_comap` `Filter.Eventually.mono`
`mono_left` 📖	mathematical	`UniformCauchySeqOnFilter` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`UniformCauchySeqOnFilter`	—	`Filter.Eventually.filter_mono` `Filter.prod_mono_left` `Filter.prod_mono`
`mono_right` 📖	mathematical	`UniformCauchySeqOnFilter` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`UniformCauchySeqOnFilter`	—	`Filter.Eventually.filter_mono` `Filter.prod_mono_right` `Filter.Eventually.mono`
`tendstoUniformlyOnFilter_of_tendsto` 📖	mathematical	`UniformCauchySeqOnFilter` `Filter.Eventually` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	`TendstoUniformlyOnFilter`	—	`Filter.eq_or_neBot` `Filter.bot_prod` `comp_symm_of_uniformity` `Filter.eventually_prod_iff` `Filter.eventually_swap_iff` `Filter.Tendsto.eventually` `Filter.tendsto_prodAssoc` `Filter.tendsto_prod_swap` `Filter.Eventually.and` `Filter.Eventually.mono` `Filter.Eventually.curry` `Set.mem_of_mem_of_subset` `Uniform.tendsto_nhds_right` `Filter.Eventually.exists`

UniformContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_tendstoUniformly` 📖	mathematical	`UniformContinuous` `TendstoUniformly`	`TendstoUniformly`	—	—
`comp_tendstoUniformlyOn` 📖	mathematical	`UniformContinuous` `TendstoUniformlyOn`	`TendstoUniformlyOn`	—	—
`comp_tendstoUniformlyOnFilter` 📖	mathematical	`UniformContinuous` `TendstoUniformlyOnFilter`	`TendstoUniformlyOnFilter`	—	—
`comp_uniformCauchySeqOn` 📖	mathematical	`UniformContinuous` `UniformCauchySeqOn`	`UniformCauchySeqOn`	—	—

UniformContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoUniformly` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `UniformContinuousOn` `instUniformSpaceProd` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase` `SProd.sprod` `Set.instSProd` `Set.univ`	`TendstoUniformly` `nhds` `UniformSpace.toTopologicalSpace`	—	`nhdsWithin_eq_nhds` `tendstoUniformlyOn` `mem_of_mem_nhds`
`tendstoUniformlyOn` 📖	mathematical	`UniformContinuousOn` `instUniformSpaceProd` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase` `SProd.sprod` `Set` `Set.instSProd` `Set.instMembership`	`TendstoUniformlyOn` `nhdsWithin` `UniformSpace.toTopologicalSpace`	—	`tendstoUniformlyOn_iff_tendsto` `Filter.comap_inf` `Filter.comap_principal` `inf_assoc` `Filter.inf_principal` `Filter.Tendsto.comp` `Filter.Tendsto.inf` `nhds_eq_comap_uniformity` `Filter.comap_comap` `uniformity_prod_eq_comap_prod` `Filter.Tendsto.prodMk` `Filter.tendsto_comap` `tendsto_diag_uniformity` `Filter.tendsto_principal_principal`

UniformContinuous₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoUniformly` 📖	mathematical	`UniformContinuous₂`	`TendstoUniformly` `nhds` `UniformSpace.toTopologicalSpace`	—	`UniformContinuousOn.tendstoUniformly` `Filter.univ_mem` `Set.univ_prod_univ` `uniformContinuousOn_univ`

(root)

Definitions

Name	Category	Theorems
`TendstoUniformly` 📖	MathDef	55 math math: `tendstoUniformly_iff_tendstoUniformlyOnFilter`, `TendstoUniformly.im`, `TendstoUniformly.inv`, `tendstoUniformly_iff_tendsto`, `HasSumUniformly.tendstoUniformlyOn_finsetRange`, `tendstoUniformlyOn_univ`, `tendstoUniformly_tsum_nat`, `tendstoUniformly_iff_seq_tendstoUniformly`, `tendstoUniformly_tsum_of_cofinite_eventually`, `UniformContinuousOn.comp_tendstoUniformly_eventually`, `hasSumUniformly_iff_tendstoUniformly`, `TendstoUniformly.prodMk`, `tendstoUniformly_congr_inseparable`, `TendstoUniformly.fun_mul`, `TendstoUniformly.fun_add`, `EMetric.tendstoUniformly_iff`, `Antitone.tendstoUniformly_of_forall_tendsto`, `TendstoUniformly.mul`, `UniformFun.tendsto_iff_tendstoUniformly`, `UniformContinuous₂.tendstoUniformly`, `IsTopologicalGroup.tendstoUniformly_iff`, `Filter.HasBasis.tendstoUniformly_iff_of_uniformity`, `tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace`, `HasSumUniformly.tendstoUniformly`, `Filter.HasBasis.tendstoUniformly_iff`, `ContinuousMap.tendsto_iff_tendstoUniformly`, `TendstoUniformly.add`, `TendstoUniformly.fun_neg`, `tendsto_prod_top_iff`, `hasProdUniformly_iff_tendstoUniformly`, `TendstoUniformly.comp`, `TendstoUniformly.fun_sub`, `UniformContinuousOn.comp_tendstoUniformly`, `tendstoUniformlyOn_iff_restrict`, `TendstoUniformly.fun_inv`, `ContinuousOn.tendstoUniformly`, `Continuous.tendstoUniformly`, `tendstoUniformlyOn_iff_tendstoUniformly_comp_coe`, `TendstoUniformly.prodMap`, `TendstoUniformly.re`, `tendstoUniformly_congr`, `TendstoUniformly.sub`, `TendstoUniformly.fun_div`, `ZeroAtInftyContinuousMap.tendsto_iff_tendstoUniformly`, `Monotone.tendstoUniformly_of_forall_tendsto`, `tendstoUniformly_tsum`, `HasProdUniformly.tendstoUniformlyOn_finsetRange`, `HasProdUniformly.tendstoUniformly`, `TendstoUniformly.div`, `UniformContinuousOn.tendstoUniformly`, `IsTopologicalAddGroup.tendstoUniformly_iff`, `BoundedContinuousFunction.tendsto_iff_tendstoUniformly`, `Metric.tendstoUniformly_iff`, `UniformContinuous.comp_tendstoUniformly`, `TendstoUniformly.neg`
`TendstoUniformlyOn` 📖	MathDef	83 math math: `TendstoUniformlyOn.fun_add`, `MeasureTheory.Egorov.tendstoUniformlyOn_diff_iUnionNotConvergentSeq`, `TendstoUniformlyOn.congr`, `TendstoUniformlyOn.seq_tendstoUniformlyOn`, `Antitone.tendstoUniformlyOn_of_forall_tendsto`, `tendstoUniformlyOn_univ`, `Filter.Tendsto.tendstoUniformlyOn_const`, `TendstoUniformlyOn.comp`, `tendstoUniformlyOn_iff_tendsto`, `TendstoUniformlyOn.congr_inseparable`, `tendstoLocallyUniformly_iff_forall_isCompact`, `TendstoUniformlyOn.neg`, `TendstoUniformlyOn.congr_right`, `tendstoUniformlyOn_iff_tendstoUniformlyOnFilter`, `UniformOnFun.tendsto_iff_tendstoUniformlyOn`, `TendstoUniformlyOn.mono`, `tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact`, `SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero`, `tendstoUniformlyOn_tsum`, `Monotone.tendstoUniformlyOn_of_forall_tendsto`, `IsTopologicalGroup.tendstoUniformlyOn_iff`, `tendstoUniformlyOn_singleton_iff_tendsto`, `tendstoUniformlyOn_tsum_nat`, `TendstoUniformlyOn.mul`, `tendstoUniformlyOn_iff_seq_tendstoUniformlyOn`, `TendstoUniformly.tendstoUniformlyOn`, `SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one`, `TendstoUniformlyOn.fun_inv`, `Filter.HasBasis.tendstoUniformlyOn_iff_of_uniformity`, `HasFPowerSeriesOnBall.tendstoUniformlyOn`, `MeasureTheory.tendstoUniformlyOn_of_ae_tendsto'`, `UniformContinuous.comp_tendstoUniformlyOn`, `HasProdUniformlyOn.tendstoUniformlyOn_finsetRange`, `Metric.tendstoUniformlyOn_iff`, `ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn`, `HasFPowerSeriesOnBall.tendstoUniformlyOn'`, `tendstoUniformlyOn_of_seq_tendstoUniformlyOn`, `TendstoUniformlyOn.fun_sub`, `HasSumUniformlyOn.tendstoUniformlyOn_finsetRange`, `tendstoUniformlyOn_tsum_of_cofinite_eventually`, `Filter.HasBasis.tendstoUniformlyOn_iff`, `TendstoUniformlyOn.fun_mul`, `TendstoUniformlyOn.im`, `TendstoUniformlyOnFilter.tendstoUniformlyOn`, `tendstoUniformlyOn_iff_restrict`, `TendstoUniformlyOn.prodMk`, `MeasureTheory.tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist'`, `UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto`, `TendstoUniformlyOn.re`, `TendstoUniformlyOn.sub`, `tendstoUniformlyOn_empty`, `HasFPowerSeriesWithinOnBall.tendstoUniformlyOn`, `TendstoUniformlyOn.cderiv`, `tendstoLocallyUniformlyOn_iff_forall_isCompact`, `TendstoUniformlyOn.fun_neg`, `TendstoUniformlyOn.comp_cexp`, `tendstoUniformlyOn_iff_tendstoUniformly_comp_coe`, `MeasureTheory.tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist`, `TendstoUniformlyOn.fun_div`, `TendstoUniformlyOn.prodMap`, `HasFPowerSeriesWithinOnBall.tendstoUniformlyOn'`, `TendstoUniformlyOn.inv`, `EMetric.tendstoUniformlyOn_iff`, `UniformConvergenceCLM.tendsto_iff_tendstoUniformlyOn`, `ContinuousOn.tendsto_restrict_iff_tendstoUniformlyOn`, `hasProdUniformlyOn_iff_tendstoUniformlyOn`, `TendstoUniformlyOn.add`, `UniformContinuousOn.tendstoUniformlyOn`, `HasProdUniformlyOn.tendstoUniformlyOn`, `hasSumUniformlyOn_iff_tendstoUniformlyOn`, `Complex.exists_cthickening_tendstoUniformlyOn`, `IsTopologicalAddGroup.tendstoUniformlyOn_iff`, `HasSumUniformlyOn.tendstoUniformlyOn`, `TendstoUniformlyOn.congr_inseparable_right`, `Complex.tendstoUniformlyOn_deriv_of_cthickening_subset`, `SeminormedAddGroup.tendstoUniformlyOn_zero`, `tendstoUniformlyOn_tsum_nat_eventually`, `UniformContinuousOn.comp_tendstoUniformlyOn_eventually`, `TendstoUniformlyOn.div`, `Summable.tendstoUniformlyOn_tsum_nat_log_one_add`, `tendsto_prod_principal_iff`, `MeasureTheory.tendstoUniformlyOn_of_ae_tendsto`, `SeminormedGroup.tendstoUniformlyOn_one`
`TendstoUniformlyOnFilter` 📖	MathDef	36 math math: `tendstoUniformly_iff_tendstoUniformlyOnFilter`, `TendstoUniformlyOnFilter.mono_left`, `SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one`, `TendstoUniformlyOnFilter.mono_right`, `difference_quotients_converge_uniformly`, `Filter.HasBasis.tendstoUniformlyOnFilter_iff`, `Filter.Tendsto.tendstoUniformlyOnFilter_const`, `tendstoUniformlyOn_iff_tendstoUniformlyOnFilter`, `tendsto_prod_filter_iff`, `SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero`, `TendstoUniformlyOnFilter.prodMk`, `TendstoUniformlyOnFilter.mul`, `TendstoUniformlyOnFilter.fun_sub`, `UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto`, `TendstoUniformlyOnFilter.prodMap`, `TendstoUniformlyOnFilter.fun_inv`, `tendstoUniformlyOnFilter_iff_tendsto`, `UniformContinuous.comp_tendstoUniformlyOnFilter`, `TendstoUniformlyOnFilter.fun_div`, `TendstoUniformly.tendstoUniformlyOnFilter`, `TendstoUniformlyOnFilter.comp`, `TendstoUniformlyOnFilter.fun_mul`, `TendstoUniformlyOnFilter.inv`, `TendstoUniformlyOnFilter.fun_add`, `TendstoUniformlyOnFilter.add`, `TendstoUniformlyOnFilter.neg`, `Metric.tendstoUniformlyOnFilter_iff`, `Filter.HasBasis.tendstoUniformlyOnFilter_iff_of_uniformity`, `tendstoLocallyUniformlyOn_iff_filter`, `TendstoUniformlyOnFilter.sub`, `TendstoUniformlyOnFilter.div`, `TendstoUniformlyOnFilter.congr`, `TendstoUniformlyOnFilter.congr_inseparable`, `TendstoUniformlyOnFilter.fun_neg`, `tendstoLocallyUniformly_iff_filter`, `TendstoUniformlyOn.tendstoUniformlyOnFilter`
`UniformCauchySeqOn` 📖	MathDef	25 math math: `UniformCauchySeqOn.fun_mul`, `TendstoUniformlyOn.uniformCauchySeqOn`, `UniformCauchySeqOn.inv`, `uniformCauchySeqOn_ball_of_deriv`, `UniformCauchySeqOn.mul`, `UniformCauchySeqOn.prod`, `UniformCauchySeqOn.fun_inv`, `UniformCauchySeqOn.add`, `uniformCauchySeqOn_iff_uniformCauchySeqOnFilter`, `UniformCauchySeqOn.fun_add`, `UniformCauchySeqOn.prod'`, `SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero`, `SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one`, `UniformCauchySeqOn.fun_div`, `UniformCauchySeqOn.comp`, `UniformCauchySeqOn.fun_neg`, `UniformCauchySeqOn.neg`, `UniformCauchySeqOn.sub`, `UniformContinuous.comp_uniformCauchySeqOn`, `UniformCauchySeqOn.mono`, `uniformCauchySeqOn_ball_of_fderiv`, `UniformCauchySeqOn.fun_sub`, `UniformCauchySeqOn.div`, `UniformCauchySeqOn.prodMap`, `Metric.uniformCauchySeqOn_iff`
`UniformCauchySeqOnFilter` 📖	MathDef	11 math math: `SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one`, `uniformCauchySeqOnFilter_of_deriv`, `uniformCauchySeqOn_iff_uniformCauchySeqOnFilter`, `SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero`, `uniformCauchySeqOnFilter_of_fderiv`, `UniformCauchySeqOnFilter.mono_right`, `UniformCauchySeqOnFilter.mono_left`, `UniformCauchySeqOn.uniformCauchySeqOnFilter`, `TendstoUniformlyOnFilter.uniformCauchySeqOnFilter`, `UniformCauchySeqOnFilter.comp`, `UniformCauchySeqOnFilter.one_smulRight`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoUniformlyOnFilter_iff_tendsto` 📖	mathematical	—	`TendstoUniformlyOnFilter` `Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd` `uniformity`	—	—
`tendstoUniformlyOn_empty` 📖	mathematical	—	`TendstoUniformlyOn` `Set` `Set.instEmptyCollection`	—	`instIsEmptyFalse`
`tendstoUniformlyOn_iff_restrict` 📖	mathematical	—	`TendstoUniformlyOn` `TendstoUniformly` `Set.Elem` `Set.restrict`	—	`tendstoUniformlyOn_iff_tendstoUniformly_comp_coe`
`tendstoUniformlyOn_iff_seq_tendstoUniformlyOn` 📖	mathematical	—	`TendstoUniformlyOn` `Filter.atTop` `Nat.instPreorder`	—	`TendstoUniformlyOn.seq_tendstoUniformlyOn` `tendstoUniformlyOn_of_seq_tendstoUniformlyOn`
`tendstoUniformlyOn_iff_tendsto` 📖	mathematical	—	`TendstoUniformlyOn` `Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd` `Filter.principal` `uniformity`	—	—
`tendstoUniformlyOn_iff_tendstoUniformlyOnFilter` 📖	mathematical	—	`TendstoUniformlyOn` `TendstoUniformlyOnFilter` `Filter.principal`	—	—
`tendstoUniformlyOn_iff_tendstoUniformly_comp_coe` 📖	mathematical	—	`TendstoUniformlyOn` `TendstoUniformly` `Set.Elem` `Set` `Set.instMembership`	—	—
`tendstoUniformlyOn_of_seq_tendstoUniformlyOn` 📖	mathematical	`TendstoUniformlyOn` `Filter.atTop` `Nat.instPreorder`	`TendstoUniformlyOn`	—	`tendstoUniformlyOn_iff_tendsto` `Filter.tendsto_iff_seq_tendsto` `Filter.prod.isCountablyGenerated` `Filter.isCountablyGenerated_principal` `Filter.Tendsto.comp` `Filter.tendsto_prod_iff'` `Filter.Tendsto.prodMk` `Filter.tendsto_id`
`tendstoUniformlyOn_singleton_iff_tendsto` 📖	mathematical	—	`TendstoUniformlyOn` `Set` `Set.instSingletonSet` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	—	`Filter.principal_singleton` `Filter.prod_pure`
`tendstoUniformlyOn_univ` 📖	mathematical	—	`TendstoUniformlyOn` `Set.univ` `TendstoUniformly`	—	—
`tendstoUniformly_congr` 📖	mathematical	`Filter.EventuallyEq`	`TendstoUniformly`	—	`tendstoUniformly_congr_inseparable` `Filter.Eventually.mono` `Inseparable.of_eq`
`tendstoUniformly_congr_inseparable` 📖	mathematical	`Filter.Eventually`	`TendstoUniformly`	—	`tendstoUniformlyOn_univ` `TendstoUniformlyOn.congr_inseparable` `Filter.Eventually.mono` `Inseparable.symm`
`tendstoUniformly_iff_seq_tendstoUniformly` 📖	mathematical	—	`TendstoUniformly` `Filter.atTop` `Nat.instPreorder`	—	`tendstoUniformlyOn_iff_seq_tendstoUniformlyOn`
`tendstoUniformly_iff_tendsto` 📖	mathematical	—	`TendstoUniformly` `Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd` `Top.top` `Filter.instTop` `uniformity`	—	—
`tendstoUniformly_iff_tendstoUniformlyOnFilter` 📖	mathematical	—	`TendstoUniformly` `TendstoUniformlyOnFilter` `Top.top` `Filter` `Filter.instTop`	—	`tendstoUniformlyOn_univ` `tendstoUniformlyOn_iff_tendstoUniformlyOnFilter` `Filter.principal_univ`
`tendsto_prod_filter_iff` 📖	mathematical	—	`Filter.Tendsto` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `UniformSpace.toTopologicalSpace` `TendstoUniformlyOnFilter`	—	`nhds_eq_comap_uniformity`
`tendsto_prod_principal_iff` 📖	mathematical	—	`Filter.Tendsto` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase` `SProd.sprod` `Filter` `Filter.instSProd` `Filter.principal` `nhds` `UniformSpace.toTopologicalSpace` `TendstoUniformlyOn`	—	`tendstoUniformlyOn_iff_tendstoUniformlyOnFilter` `tendsto_prod_filter_iff`
`tendsto_prod_top_iff` 📖	mathematical	—	`Filter.Tendsto` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase` `SProd.sprod` `Filter` `Filter.instSProd` `Top.top` `Filter.instTop` `nhds` `UniformSpace.toTopologicalSpace` `TendstoUniformly`	—	`tendstoUniformly_iff_tendstoUniformlyOnFilter` `tendsto_prod_filter_iff`
`uniformCauchySeqOn_iff_uniformCauchySeqOnFilter` 📖	mathematical	—	`UniformCauchySeqOn` `UniformCauchySeqOnFilter` `Filter.principal`	—	`Filter.eventually_prod_principal_iff`

---

← Back to Index