Documentation Verification Report

LocallyUniformConvergence

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

Statistics

Metric	Count
Definitions `TendstoLocallyUniformly`, `TendstoLocallyUniformlyOn`	2
Theorems `tendstoLocallyUniformlyOn_iff_forall_tendsto`, `comp`, `congr_inseparable`, `congr_inseparable_right`, `congr_right`, `piProd`, `prodMk`, `tendstoLocallyUniformlyOn`, `comp`, `congr_inseparable`, `congr_inseparable_right`, `congr_right`, `mono`, `piProd`, `prodMk`, `tendsto_at`, `union`, `unique`, `tendstoLocallyUniformly`, `tendstoLocallyUniformlyOn`, `comp_tendstoLocallyUniformly`, `comp_tendstoLocallyUniformlyOn`, `comp_tendstoLocallyUniformly`, `comp_tendstoLocallyUniformlyOn`, `tendstoLocallyUniformlyOn_TFAE`, `tendstoLocallyUniformlyOn_biUnion`, `tendstoLocallyUniformlyOn_iUnion`, `tendstoLocallyUniformlyOn_iff_filter`, `tendstoLocallyUniformlyOn_iff_forall_isCompact`, `tendstoLocallyUniformlyOn_iff_forall_tendsto`, `tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe`, `tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact`, `tendstoLocallyUniformlyOn_of_forall_exists_nhds`, `tendstoLocallyUniformlyOn_sUnion`, `tendstoLocallyUniformlyOn_univ`, `tendstoLocallyUniformly_iff_filter`, `tendstoLocallyUniformly_iff_forall_isCompact`, `tendstoLocallyUniformly_iff_forall_tendsto`, `tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace`, `tendstoLocallyUniformly_of_forall_exists_nhds`	40
Total	42

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoLocallyUniformlyOn_iff_forall_tendsto` 📖	mathematical	`IsOpen`	`TendstoLocallyUniformlyOn` `Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `uniformity`	—	`tendstoLocallyUniformlyOn_iff_forall_tendsto` `nhdsWithin_eq`

TendstoLocallyUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`TendstoLocallyUniformly` `Continuous`	—	—	`tendstoLocallyUniformlyOn_univ` `TendstoLocallyUniformlyOn.comp` `Set.mapsTo_univ` `continuousOn_univ`
`congr_inseparable` 📖	—	`TendstoLocallyUniformly` `Filter.Eventually`	—	—	`tendstoLocallyUniformlyOn_univ` `TendstoLocallyUniformlyOn.congr_inseparable` `tendstoLocallyUniformlyOn`
`congr_inseparable_right` 📖	—	`TendstoLocallyUniformly` `Inseparable` `UniformSpace.toTopologicalSpace`	—	—	`tendstoLocallyUniformlyOn_univ` `TendstoLocallyUniformlyOn.congr_inseparable_right` `tendstoLocallyUniformlyOn`
`congr_right` 📖	—	`TendstoLocallyUniformly`	—	—	`congr_inseparable_right` `Inseparable.of_eq`
`piProd` 📖	mathematical	`TendstoLocallyUniformly`	`instUniformSpaceProd` `Pi.prod`	—	`prodMk`
`prodMk` 📖	mathematical	`TendstoLocallyUniformly`	`instUniformSpaceProd`	—	`tendstoLocallyUniformlyOn_univ` `TendstoLocallyUniformlyOn.prodMk`
`tendstoLocallyUniformlyOn` 📖	mathematical	`TendstoLocallyUniformly`	`TendstoLocallyUniformlyOn`	—	`TendstoLocallyUniformlyOn.mono` `tendstoLocallyUniformlyOn_univ` `Set.subset_univ`

TendstoLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`TendstoLocallyUniformlyOn` `Set.MapsTo` `ContinuousOn`	—	—	`ContinuousWithinAt.preimage_mem_nhdsWithin'` `nhdsWithin_mono` `Set.MapsTo.image_subset` `Filter.Eventually.mono`
`congr_inseparable` 📖	—	`TendstoLocallyUniformlyOn` `Filter.Eventually`	—	—	`Filter.eventually_prod_principal_iff` `tendstoLocallyUniformlyOn_iff_forall_tendsto` `forall₂_imp` `Filter.HasBasis.tendsto_right_iff` `uniformity_hasBasis_open` `Filter.Eventually.mp` `Filter.Eventually.mono` `Filter.Eventually.filter_mono` `Filter.prod_mono_right` `inf_le_right` `Inseparable.mem_open_iff` `Inseparable.prod` `Inseparable.rfl`
`congr_inseparable_right` 📖	—	`TendstoLocallyUniformlyOn` `Inseparable` `UniformSpace.toTopologicalSpace`	—	—	`Filter.eventually_prod_principal_iff` `Filter.Eventually.of_forall` `tendstoLocallyUniformlyOn_iff_forall_tendsto` `forall₂_imp` `Filter.HasBasis.tendsto_right_iff` `uniformity_hasBasis_open` `Filter.Eventually.mp` `Filter.Eventually.mono` `Filter.Eventually.filter_mono` `Filter.prod_mono_right` `inf_le_right` `Inseparable.mem_open_iff` `Inseparable.prod` `Inseparable.rfl`
`congr_right` 📖	—	`TendstoLocallyUniformlyOn` `Set.EqOn`	—	—	`congr_inseparable_right` `Inseparable.of_eq`
`mono` 📖	—	`TendstoLocallyUniformlyOn` `Set` `Set.instHasSubset`	—	—	`nhdsWithin_mono` `Filter.Eventually.mono`
`piProd` 📖	mathematical	`TendstoLocallyUniformlyOn`	`instUniformSpaceProd` `Pi.prod`	—	`prodMk`
`prodMk` 📖	mathematical	`TendstoLocallyUniformlyOn`	`instUniformSpaceProd`	—	`tendstoLocallyUniformlyOn_iff_forall_tendsto` `uniformity_prod_eq_comap_prod` `Filter.tendsto_comap_iff` `Filter.Tendsto.prodMk`
`tendsto_at` 📖	mathematical	`TendstoLocallyUniformlyOn` `Set` `Set.instMembership`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	—	`TendstoUniformlyOnFilter.tendsto_at` `tendstoLocallyUniformlyOn_iff_filter` `Filter.principal_singleton` `pure_le_nhdsWithin`
`union` 📖	mathematical	`IsOpen` `TendstoLocallyUniformlyOn`	`Set` `Set.instUnion`	—	`Set.sUnion_pair` `tendstoLocallyUniformlyOn_sUnion`
`unique` 📖	mathematical	`TendstoLocallyUniformlyOn`	`Set.EqOn`	—	`tendsto_nhds_unique` `tendsto_at`

TendstoUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoLocallyUniformly` 📖	mathematical	`TendstoUniformly`	`TendstoLocallyUniformly`	—	`Filter.univ_mem`

TendstoUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoLocallyUniformlyOn` 📖	mathematical	`TendstoUniformlyOn`	`TendstoLocallyUniformlyOn`	—	`self_mem_nhdsWithin`

UniformContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_tendstoLocallyUniformly` 📖	—	`UniformContinuous` `TendstoLocallyUniformly`	—	—	`UniformContinuousOn.comp_tendstoLocallyUniformly` `uniformContinuousOn`
`comp_tendstoLocallyUniformlyOn` 📖	—	`UniformContinuous` `TendstoLocallyUniformlyOn`	—	—	`UniformContinuousOn.comp_tendstoLocallyUniformlyOn` `uniformContinuousOn` `Set.mapsTo_univ` `Filter.Eventually.of_forall`

UniformContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_tendstoLocallyUniformly` 📖	—	`UniformContinuousOn` `TendstoLocallyUniformly` `Set` `Set.instMembership` `Filter.Eventually`	—	—	`tendstoLocallyUniformlyOn_univ` `comp_tendstoLocallyUniformlyOn`
`comp_tendstoLocallyUniformlyOn` 📖	—	`UniformContinuousOn` `TendstoLocallyUniformlyOn` `Set.MapsTo` `Filter.Eventually`	—	—	`tendstoLocallyUniformlyOn_iff_forall_tendsto` `Filter.Tendsto.comp` `Filter.tendsto_inf` `Filter.tendsto_principal` `Filter.mp_mem` `eventually_mem_nhdsWithin` `Filter.univ_mem'`

(root)

Definitions

Name	Category	Theorems
`TendstoLocallyUniformly` 📖	MathDef	20 math math: `IsTopologicalGroup.tendstoLocallyUniformly_iff`, `tendstoLocallyUniformly_iff_forall_isCompact`, `hasProdLocallyUniformly_iff_tendstoLocallyUniformly`, `HasSumLocallyUniformly.tendstoLocallyUniformly_finsetRange`, `tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace`, `HasProdLocallyUniformly.tendstoLocallyUniformly_finsetRange`, `tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe`, `Antitone.tendstoLocallyUniformly_of_forall_tendsto`, `EMetric.tendstoLocallyUniformly_iff`, `ContinuousMap.tendsto_iff_tendstoLocallyUniformly`, `TendstoUniformly.tendstoLocallyUniformly`, `tendstoLocallyUniformly_iff_forall_tendsto`, `tendstoLocallyUniformly_of_forall_exists_nhds`, `Monotone.tendstoLocallyUniformly_of_forall_tendsto`, `Metric.tendstoLocallyUniformly_iff`, `tendstoLocallyUniformlyOn_univ`, `hasSumLocallyUniformly_iff_tendstoLocallyUniformly`, `tendstoLocallyUniformly_iff_filter`, `EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly`, `IsTopologicalAddGroup.tendstoLocallyUniformly_iff`
`TendstoLocallyUniformlyOn` 📖	MathDef	27 math math: `IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto`, `HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn`, `HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn`, `EMetric.tendstoLocallyUniformlyOn_iff`, `hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn`, `tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact`, `HasSumLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange`, `IsTopologicalAddGroup.tendstoLocallyUniformlyOn_iff`, `TendstoLocallyUniformly.tendstoLocallyUniformlyOn`, `hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn`, `HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn'`, `tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe`, `tendstoLocallyUniformlyOn_of_forall_exists_nhds`, `tendstoLocallyUniformlyOn_TFAE`, `HasProdLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange`, `Real.tendstoLocallyUniformlyOn_rpow_sub_one_log`, `Metric.tendstoLocallyUniformlyOn_iff`, `IsTopologicalGroup.tendstoLocallyUniformlyOn_iff`, `tendstoLocallyUniformlyOn_iff_forall_isCompact`, `EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn`, `Monotone.tendstoLocallyUniformlyOn_of_forall_tendsto`, `tendstoLocallyUniformlyOn_iff_filter`, `TendstoUniformlyOn.tendstoLocallyUniformlyOn`, `HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn'`, `Antitone.tendstoLocallyUniformlyOn_of_forall_tendsto`, `tendstoLocallyUniformlyOn_univ`, `tendstoLocallyUniformlyOn_iff_forall_tendsto`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoLocallyUniformlyOn_TFAE` 📖	mathematical	`IsOpen`	`List.TFAE` `TendstoLocallyUniformlyOn`	—	`tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact` `TendstoLocallyUniformlyOn.mono` `Filter.HasBasis.mem_iff` `compact_basis_nhds` `IsOpen.mem_nhds` `nhdsWithin_le_nhds` `List.tfae_of_cycle`
`tendstoLocallyUniformlyOn_biUnion` 📖	mathematical	`IsOpen` `TendstoLocallyUniformlyOn`	`Set.iUnion` `Set` `Set.instMembership`	—	`tendstoLocallyUniformlyOn_iUnion` `isOpen_iUnion`
`tendstoLocallyUniformlyOn_iUnion` 📖	mathematical	`IsOpen` `TendstoLocallyUniformlyOn`	`Set.iUnion`	—	`IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto` `isOpen_iUnion` `Set.mem_iUnion`
`tendstoLocallyUniformlyOn_iff_filter` 📖	mathematical	—	`TendstoLocallyUniformlyOn` `TendstoUniformlyOnFilter` `nhdsWithin`	—	`Filter.eventually_of_mem`
`tendstoLocallyUniformlyOn_iff_forall_isCompact` 📖	mathematical	`IsOpen`	`TendstoLocallyUniformlyOn` `TendstoUniformlyOn`	—	`List.TFAE.out` `tendstoLocallyUniformlyOn_TFAE`
`tendstoLocallyUniformlyOn_iff_forall_tendsto` 📖	mathematical	—	`TendstoLocallyUniformlyOn` `Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd` `nhdsWithin` `uniformity`	—	`forall₂_swap`
`tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe` 📖	mathematical	—	`TendstoLocallyUniformlyOn` `TendstoLocallyUniformly` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Filter.prod_map_right`
`tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact` 📖	mathematical	`IsCompact`	`TendstoLocallyUniformlyOn` `TendstoUniformlyOn`	—	`tendstoUniformlyOn_iff_tendstoUniformly_comp_coe` `tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace` `isCompact_iff_compactSpace` `tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe` `TendstoUniformlyOn.tendstoLocallyUniformlyOn`
`tendstoLocallyUniformlyOn_of_forall_exists_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `TendstoUniformlyOn`	`TendstoLocallyUniformlyOn`	—	`tendstoLocallyUniformlyOn_iff_forall_tendsto` `Filter.Tendsto.mono_left` `tendstoUniformlyOn_iff_tendsto` `Filter.prod_mono_right` `Filter.le_principal_iff`
`tendstoLocallyUniformlyOn_sUnion` 📖	mathematical	`IsOpen` `TendstoLocallyUniformlyOn`	`Set.sUnion`	—	`Set.sUnion_eq_biUnion` `tendstoLocallyUniformlyOn_biUnion`
`tendstoLocallyUniformlyOn_univ` 📖	mathematical	—	`TendstoLocallyUniformlyOn` `Set.univ` `TendstoLocallyUniformly`	—	`nhdsWithin_univ`
`tendstoLocallyUniformly_iff_filter` 📖	mathematical	—	`TendstoLocallyUniformly` `TendstoUniformlyOnFilter` `nhds`	—	`tendstoLocallyUniformlyOn_iff_filter`
`tendstoLocallyUniformly_iff_forall_isCompact` 📖	mathematical	—	`TendstoLocallyUniformly` `TendstoUniformlyOn`	—	`tendstoLocallyUniformlyOn_iff_forall_isCompact` `isOpen_univ`
`tendstoLocallyUniformly_iff_forall_tendsto` 📖	mathematical	—	`TendstoLocallyUniformly` `Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `uniformity`	—	`IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto` `isOpen_univ`
`tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace` 📖	mathematical	—	`TendstoLocallyUniformly` `TendstoUniformly`	—	`IsCompact.elim_nhds_subcover'` `isCompact_univ` `Filter.Eventually.mono` `Filter.eventually_all` `Finite.of_fintype` `Set.mem_univ` `TendstoUniformly.tendstoLocallyUniformly`
`tendstoLocallyUniformly_of_forall_exists_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `TendstoUniformlyOn`	`TendstoLocallyUniformly`	—	`tendstoLocallyUniformlyOn_univ` `tendstoLocallyUniformlyOn_of_forall_exists_nhds` `nhdsWithin_univ`

---

← Back to Index