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` 📖	mathematical	`TendstoLocallyUniformly` `Continuous`	`TendstoLocallyUniformly`	—	`tendstoLocallyUniformlyOn_univ` `TendstoLocallyUniformlyOn.comp` `Set.mapsTo_univ` `continuousOn_univ`
`congr_inseparable` 📖	mathematical	`TendstoLocallyUniformly` `Filter.Eventually`	`TendstoLocallyUniformly`	—	`tendstoLocallyUniformlyOn_univ` `TendstoLocallyUniformlyOn.congr_inseparable` `tendstoLocallyUniformlyOn`
`congr_inseparable_right` 📖	mathematical	`TendstoLocallyUniformly` `Inseparable` `UniformSpace.toTopologicalSpace`	`TendstoLocallyUniformly`	—	`tendstoLocallyUniformlyOn_univ` `TendstoLocallyUniformlyOn.congr_inseparable_right` `tendstoLocallyUniformlyOn`
`congr_right` 📖	mathematical	`TendstoLocallyUniformly`	`TendstoLocallyUniformly`	—	`congr_inseparable_right` `Inseparable.of_eq`
`piProd` 📖	mathematical	`TendstoLocallyUniformly`	`TendstoLocallyUniformly` `instUniformSpaceProd` `Pi.prod`	—	`prodMk`
`prodMk` 📖	mathematical	`TendstoLocallyUniformly`	`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` 📖	mathematical	`TendstoLocallyUniformlyOn` `Set.MapsTo` `ContinuousOn`	`TendstoLocallyUniformlyOn`	—	`ContinuousWithinAt.preimage_mem_nhdsWithin'` `nhdsWithin_mono` `Set.MapsTo.image_subset` `Filter.Eventually.mono`
`congr_inseparable` 📖	mathematical	`TendstoLocallyUniformlyOn` `Filter.Eventually`	`TendstoLocallyUniformlyOn`	—	`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` 📖	mathematical	`TendstoLocallyUniformlyOn` `Inseparable` `UniformSpace.toTopologicalSpace`	`TendstoLocallyUniformlyOn`	—	`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` 📖	mathematical	`TendstoLocallyUniformlyOn` `Set.EqOn`	`TendstoLocallyUniformlyOn`	—	`congr_inseparable_right` `Inseparable.of_eq`
`mono` 📖	mathematical	`TendstoLocallyUniformlyOn` `Set` `Set.instHasSubset`	`TendstoLocallyUniformlyOn`	—	`nhdsWithin_mono` `Filter.Eventually.mono`
`piProd` 📖	mathematical	`TendstoLocallyUniformlyOn`	`TendstoLocallyUniformlyOn` `instUniformSpaceProd` `Pi.prod`	—	`prodMk`
`prodMk` 📖	mathematical	`TendstoLocallyUniformlyOn`	`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`	`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` 📖	mathematical	`UniformContinuous` `TendstoLocallyUniformly`	`TendstoLocallyUniformly`	—	`UniformContinuousOn.comp_tendstoLocallyUniformly` `uniformContinuousOn`
`comp_tendstoLocallyUniformlyOn` 📖	mathematical	`UniformContinuous` `TendstoLocallyUniformlyOn`	`TendstoLocallyUniformlyOn`	—	`UniformContinuousOn.comp_tendstoLocallyUniformlyOn` `uniformContinuousOn` `Set.mapsTo_univ` `Filter.Eventually.of_forall`

UniformContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_tendstoLocallyUniformly` 📖	mathematical	`UniformContinuousOn` `TendstoLocallyUniformly` `Set` `Set.instMembership` `Filter.Eventually`	`TendstoLocallyUniformly`	—	`tendstoLocallyUniformlyOn_univ` `comp_tendstoLocallyUniformlyOn`
`comp_tendstoLocallyUniformlyOn` 📖	mathematical	`UniformContinuousOn` `TendstoLocallyUniformlyOn` `Set.MapsTo` `Filter.Eventually`	`TendstoLocallyUniformlyOn`	—	`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	55 math math: `TendstoLocallyUniformly.inv`, `TendstoLocallyUniformly.sub`, `TendstoLocallyUniformly.fun_sub`, `TendstoLocallyUniformly.fun_inv₀`, `TendstoLocallyUniformly.smul₀`, `IsTopologicalGroup.tendstoLocallyUniformly_iff`, `TendstoLocallyUniformly.fun_add`, `TendstoLocallyUniformly.smul₀_of_isBoundedUnder`, `TendstoLocallyUniformly.congr_inseparable_right`, `tendstoLocallyUniformly_iff_forall_isCompact`, `UniformContinuousOn.comp_tendstoLocallyUniformly`, `TendstoLocallyUniformly.fun_mul`, `TendstoLocallyUniformly.neg`, `TendstoLocallyUniformly.congr`, `hasProdLocallyUniformly_iff_tendstoLocallyUniformly`, `HasSumLocallyUniformly.tendstoLocallyUniformly_finsetRange`, `TendstoLocallyUniformly.congr_inseparable`, `tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace`, `TendstoLocallyUniformly.fun_smul₀`, `HasProdLocallyUniformly.tendstoLocallyUniformly_finsetRange`, `tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe`, `Antitone.tendstoLocallyUniformly_of_forall_tendsto`, `TendstoLocallyUniformly.div₀`, `EMetric.tendstoLocallyUniformly_iff`, `TendstoLocallyUniformly.fun_div`, `TendstoLocallyUniformly.fun_inv₀_of_disjoint`, `TendstoLocallyUniformly.prodMk`, `TendstoLocallyUniformly.add`, `TendstoLocallyUniformly.fun_mul₀`, `TendstoLocallyUniformly.congr_right`, `UniformContinuous.comp_tendstoLocallyUniformly`, `TendstoLocallyUniformly.fun_neg`, `ContinuousMap.tendsto_iff_tendstoLocallyUniformly`, `TendstoUniformly.tendstoLocallyUniformly`, `tendstoLocallyUniformly_iff_forall_tendsto`, `TendstoLocallyUniformly.mul`, `TendstoLocallyUniformly.inv₀_of_disjoint`, `TendstoLocallyUniformly.inv₀`, `TendstoLocallyUniformly.piProd`, `TendstoLocallyUniformly.fun_mul₀_of_isBoundedUnder`, `TendstoLocallyUniformly.fun_div₀`, `TendstoLocallyUniformly.comp`, `TendstoLocallyUniformly.div`, `TendstoLocallyUniformly.mul₀`, `TendstoLocallyUniformly.mul₀_of_isBoundedUnder`, `tendstoLocallyUniformly_of_forall_exists_nhds`, `Monotone.tendstoLocallyUniformly_of_forall_tendsto`, `TendstoLocallyUniformly.fun_inv`, `Metric.tendstoLocallyUniformly_iff`, `tendstoLocallyUniformlyOn_univ`, `hasSumLocallyUniformly_iff_tendstoLocallyUniformly`, `tendstoLocallyUniformly_iff_filter`, `TendstoLocallyUniformly.fun_smul₀_of_isBoundedUnder`, `EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly`, `IsTopologicalAddGroup.tendstoLocallyUniformly_iff`
`TendstoLocallyUniformlyOn` 📖	MathDef	68 math math: `IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto`, `HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn`, `TendstoLocallyUniformlyOn.union`, `TendstoLocallyUniformlyOn.div₀`, `TendstoLocallyUniformlyOn.inv₀`, `TendstoLocallyUniformlyOn.mul₀_of_isBoundedUnder`, `TendstoLocallyUniformlyOn.fun_inv₀_of_disjoint`, `HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn`, `TendstoLocallyUniformlyOn.fun_div₀`, `TendstoLocallyUniformlyOn.add`, `EMetric.tendstoLocallyUniformlyOn_iff`, `TendstoLocallyUniformlyOn.fun_smul₀`, `TendstoLocallyUniformlyOn.fun_inv`, `TendstoLocallyUniformlyOn.smul₀_of_isBoundedUnder`, `TendstoLocallyUniformlyOn.piProd`, `TendstoLocallyUniformlyOn.neg`, `TendstoLocallyUniformlyOn.mul`, `hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn`, `tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact`, `TendstoLocallyUniformlyOn.div`, `HasSumLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange`, `UniformContinuous.comp_tendstoLocallyUniformlyOn`, `TendstoLocallyUniformlyOn.fun_sub`, `IsTopologicalAddGroup.tendstoLocallyUniformlyOn_iff`, `TendstoLocallyUniformly.tendstoLocallyUniformlyOn`, `hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn`, `TendstoLocallyUniformlyOn.fun_div`, `TendstoLocallyUniformlyOn.deriv`, `HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn'`, `TendstoLocallyUniformlyOn.congr_inseparable`, `tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe`, `UniformContinuousOn.comp_tendstoLocallyUniformlyOn`, `TendstoLocallyUniformlyOn.fun_smul₀_of_isBoundedUnder`, `tendstoLocallyUniformlyOn_of_forall_exists_nhds`, `tendstoLocallyUniformlyOn_TFAE`, `TendstoLocallyUniformlyOn.inv₀_of_disjoint`, `tendstoLocallyUniformlyOn_biUnion`, `HasProdLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange`, `Real.tendstoLocallyUniformlyOn_rpow_sub_one_log`, `Metric.tendstoLocallyUniformlyOn_iff`, `TendstoLocallyUniformlyOn.fun_add`, `IsTopologicalGroup.tendstoLocallyUniformlyOn_iff`, `TendstoLocallyUniformlyOn.mono`, `tendstoLocallyUniformlyOn_iff_forall_isCompact`, `TendstoLocallyUniformlyOn.fun_inv₀`, `TendstoLocallyUniformlyOn.inv`, `TendstoLocallyUniformlyOn.comp`, `TendstoLocallyUniformlyOn.fun_neg`, `TendstoLocallyUniformlyOn.congr_inseparable_right`, `TendstoLocallyUniformlyOn.congr`, `TendstoLocallyUniformlyOn.prodMk`, `TendstoLocallyUniformlyOn.fun_mul`, `TendstoLocallyUniformlyOn.mul₀`, `EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn`, `TendstoLocallyUniformlyOn.smul₀`, `Monotone.tendstoLocallyUniformlyOn_of_forall_tendsto`, `tendstoLocallyUniformlyOn_sUnion`, `tendstoLocallyUniformlyOn_iff_filter`, `TendstoUniformlyOn.tendstoLocallyUniformlyOn`, `HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn'`, `TendstoLocallyUniformlyOn.fun_mul₀`, `TendstoLocallyUniformlyOn.congr_right`, `Antitone.tendstoLocallyUniformlyOn_of_forall_tendsto`, `tendstoLocallyUniformlyOn_iUnion`, `tendstoLocallyUniformlyOn_univ`, `tendstoLocallyUniformlyOn_iff_forall_tendsto`, `TendstoLocallyUniformlyOn.sub`, `TendstoLocallyUniformlyOn.fun_mul₀_of_isBoundedUnder`

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`	`TendstoLocallyUniformlyOn` `Set.iUnion` `Set` `Set.instMembership`	—	`tendstoLocallyUniformlyOn_iUnion` `isOpen_iUnion`
`tendstoLocallyUniformlyOn_iUnion` 📖	mathematical	`IsOpen` `TendstoLocallyUniformlyOn`	`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₂_comm`
`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`	`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