UniformOn

📁 Source: Mathlib/Topology/Algebra/InfiniteSum/UniformOn.lean

Statistics

Metric	Count
Definitions `HasProdLocallyUniformly`, `HasProdLocallyUniformlyOn`, `HasProdUniformly`, `HasProdUniformlyOn`, `HasSumLocallyUniformly`, `HasSumLocallyUniformlyOn`, `HasSumUniformly`, `HasSumUniformlyOn`, `MultipliableLocallyUniformly`, `MultipliableLocallyUniformlyOn`, `MultipliableUniformly`, `SummableLocallyUniformly`, `SummableLocallyUniformlyOn`, `SummableUniformly`	14
Theorems `hasProd`, `hasProdLocallyUniformlyOn`, `multipliableLocallyUniformly`, `tendstoLocallyUniformly_finsetRange`, `exists_hasProdUniformlyOn`, `hasProd`, `hasProdUniformlyOn_of_isCompact`, `mono`, `multipliableLocallyUniformlyOn`, `tendstoLocallyUniformlyOn_finsetRange`, `tprod_eqOn`, `hasProd`, `hasProdLocallyUniformly`, `hasProdUniformlyOn`, `multipliableUniformly`, `tendstoUniformly`, `tendstoUniformlyOn_finsetRange`, `congr_right`, `hasProd`, `hasProdLocallyUniformlyOn`, `mono`, `multipliableUniformlyOn`, `tendstoUniformlyOn`, `tendstoUniformlyOn_finsetRange`, `tprod_eq`, `tprod_eqOn`, `hasSum`, `hasSumLocallyUniformlyOn`, `summableLocallyUniformly`, `tendstoLocallyUniformly_finsetRange`, `hasSum`, `mono`, `summableLocallyUniformlyOn`, `tendstoLocallyUniformlyOn_finsetRange`, `tsum_eqOn`, `hasSum`, `hasSumLocallyUniformly`, `hasSumUniformlyOn`, `summableUniformly`, `tendstoUniformly`, `tendstoUniformlyOn_finsetRange`, `congr_right`, `hasSum`, `hasSumLocallyUniformlyOn`, `mono`, `summableUniformlyOn`, `tendstoUniformlyOn`, `tendstoUniformlyOn_finsetRange`, `tsum_eq`, `tsum_eqOn`, `exists`, `hasProdLocallyUniformly`, `multipliable`, `multipliableLocallyUniformlyOn`, `exists_multipliableUniformlyOn`, `hasProdLocallyUniformlyOn`, `mono`, `multipliable`, `multipliableUniformlyOn_of_isCompact`, `MultipliableLocallyUniformlyOn_congr`, `exists`, `hasProdUniformly`, `multipliable`, `multipliableUniformlyOn`, `exists`, `hasProdUniformlyOn`, `mono`, `multipliable`, `exists`, `hasSumLocallyUniformly`, `summable`, `summableLocallyUniformlyOn`, `hasSumLocallyUniformlyOn`, `mono`, `summable`, `SummableLocallyUniformlyOn_congr`, `exists`, `hasSumUniformly`, `summable`, `summableUniformlyOn`, `exists`, `hasSumUniformlyOn`, `mono`, `summable`, `hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn`, `hasProdLocallyUniformlyOn_of_forall_compact`, `hasProdLocallyUniformlyOn_of_of_forall_exists_nhds`, `hasProdLocallyUniformly_iff_tendstoLocallyUniformly`, `hasProdLocallyUniformly_of_forall_compact`, `hasProdLocallyUniformly_of_of_forall_exists_nhds`, `hasProdUniformlyOn_iff_tendstoUniformlyOn`, `hasProdUniformlyOn_univ_iff`, `hasProdUniformly_iff_tendstoUniformly`, `hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn`, `hasSumLocallyUniformlyOn_of_forall_compact`, `hasSumLocallyUniformlyOn_of_of_forall_exists_nhds`, `hasSumLocallyUniformly_iff_tendstoLocallyUniformly`, `hasSumLocallyUniformly_of_forall_compact`, `hasSumLocallyUniformly_of_of_forall_exists_nhds`, `hasSumUniformlyOn_iff_tendstoUniformlyOn`, `hasSumUniformlyOn_univ_iff`, `hasSumUniformly_iff_tendstoUniformly`, `multipliableLocallyUniformlyOn_iff_hasProdLocallyUniformlyOn`, `multipliableLocallyUniformlyOn_of_of_forall_exists_nhds`, `multipliableLocallyUniformly_iff_hasProdLocallyUniformly`, `multipliableLocallyUniformly_of_of_forall_exists_nhds`, `multipliableUniformlyOn_iff_hasProdUniformlyOn`, `multipliableUniformlyOn_univ_iff`, `multipliableUniformly_iff_hasProdUniformly`, `summableLocallyUniformlyOn_iff_hasSumLocallyUniformlyOn`, `summableLocallyUniformlyOn_of_of_forall_exists_nhds`, `summableLocallyUniformly_iff_hasSumLocallyUniformly`, `summableLocallyUniformly_of_of_forall_exists_nhds`, `summableUniformlyOn_iff_hasSumUniformlyOn`, `summableUniformlyOn_univ_iff`, `summableUniformly_iff_hasSumUniformly`	116
Total	130

HasProdLocallyUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProd` 📖	mathematical	`HasProdLocallyUniformly`	`HasProd` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`TendstoLocallyUniformlyOn.tendsto_at` `TendstoLocallyUniformly.tendstoLocallyUniformlyOn` `Set.mem_univ`
`hasProdLocallyUniformlyOn` 📖	mathematical	`HasProdLocallyUniformly`	`HasProdLocallyUniformlyOn`	—	`TendstoLocallyUniformly.tendstoLocallyUniformlyOn`
`multipliableLocallyUniformly` 📖	mathematical	`HasProdLocallyUniformly`	`MultipliableLocallyUniformly`	—	—
`tendstoLocallyUniformly_finsetRange` 📖	mathematical	`HasProdLocallyUniformly`	`TendstoLocallyUniformly` `Finset.prod` `Finset.range` `Filter.atTop` `Nat.instPreorder`	—	`HasProdLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange` `hasProdLocallyUniformlyOn`

HasProdLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_hasProdUniformlyOn` 📖	mathematical	`HasProdLocallyUniformlyOn` `Set` `Filter` `Filter.instMembership` `nhds`	`nhdsWithin` `HasProdUniformlyOn`	—	`Filter.HasBasis.mem_iff` `compact_basis_nhds` `nhdsWithin_le_nhds` `hasProdUniformlyOn_of_isCompact` `TendstoLocallyUniformlyOn.mono`
`hasProd` 📖	mathematical	`HasProdLocallyUniformlyOn` `Set` `Set.instMembership`	`HasProd` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`TendstoLocallyUniformlyOn.tendsto_at`
`hasProdUniformlyOn_of_isCompact` 📖	mathematical	`HasProdLocallyUniformlyOn` `IsCompact`	`HasProdUniformlyOn`	—	`hasProdUniformlyOn_iff_tendstoUniformlyOn` `tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact`
`mono` 📖	—	`HasProdLocallyUniformlyOn` `Set` `Set.instHasSubset`	—	—	`TendstoLocallyUniformlyOn.mono`
`multipliableLocallyUniformlyOn` 📖	mathematical	`HasProdLocallyUniformlyOn`	`MultipliableLocallyUniformlyOn`	—	—
`tendstoLocallyUniformlyOn_finsetRange` 📖	mathematical	`HasProdLocallyUniformlyOn`	`TendstoLocallyUniformlyOn` `Finset.prod` `Finset.range` `Filter.atTop` `Nat.instPreorder`	—	`hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn` `Filter.Tendsto.eventually` `Filter.tendsto_finset_range`
`tprod_eqOn` 📖	mathematical	`HasProdLocallyUniformlyOn`	`Set.EqOn` `tprod` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`HasProd.tprod_eq` `SummationFilter.instNeBotUnconditional` `hasProd`

HasProdUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProd` 📖	mathematical	`HasProdUniformly`	`HasProd` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`TendstoUniformly.tendsto_at` `tendstoUniformly`
`hasProdLocallyUniformly` 📖	mathematical	`HasProdUniformly`	`HasProdLocallyUniformly`	—	`TendstoUniformly.tendstoLocallyUniformly`
`hasProdUniformlyOn` 📖	mathematical	`HasProdUniformly`	`HasProdUniformlyOn`	—	`hasProdUniformlyOn_iff_tendstoUniformlyOn` `TendstoUniformly.tendstoUniformlyOn` `tendstoUniformly`
`multipliableUniformly` 📖	mathematical	`HasProdUniformly`	`MultipliableUniformly`	—	—
`tendstoUniformly` 📖	mathematical	`HasProdUniformly`	`TendstoUniformly` `Finset` `Finset.prod` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	`hasProdUniformly_iff_tendstoUniformly`
`tendstoUniformlyOn_finsetRange` 📖	mathematical	`HasProdUniformly`	`TendstoUniformly` `Finset.prod` `Finset.range` `Filter.atTop` `Nat.instPreorder`	—	`Filter.Tendsto.eventually` `Filter.tendsto_finset_range` `tendstoUniformly`

HasProdUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_right` 📖	—	`HasProdUniformlyOn` `Set.EqOn`	—	—	`hasProdUniformlyOn_iff_tendstoUniformlyOn` `TendstoUniformlyOn.congr_right` `tendstoUniformlyOn`
`hasProd` 📖	mathematical	`HasProdUniformlyOn` `Set` `Set.instMembership`	`HasProd` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`TendstoUniformlyOn.tendsto_at` `tendstoUniformlyOn`
`hasProdLocallyUniformlyOn` 📖	mathematical	`HasProdUniformlyOn`	`HasProdLocallyUniformlyOn`	—	`TendstoUniformlyOn.tendstoLocallyUniformlyOn`
`mono` 📖	—	`HasProdUniformlyOn` `Set` `Set.instHasSubset`	—	—	`hasProdUniformlyOn_iff_tendstoUniformlyOn` `TendstoUniformlyOn.mono` `tendstoUniformlyOn`
`multipliableUniformlyOn` 📖	mathematical	`HasProdUniformlyOn`	`MultipliableUniformlyOn`	—	—
`tendstoUniformlyOn` 📖	mathematical	`HasProdUniformlyOn`	`TendstoUniformlyOn` `Finset` `Finset.prod` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	`hasProdUniformlyOn_iff_tendstoUniformlyOn`
`tendstoUniformlyOn_finsetRange` 📖	mathematical	`HasProdUniformlyOn`	`TendstoUniformlyOn` `Finset.prod` `Finset.range` `Filter.atTop` `Nat.instPreorder`	—	`Filter.Tendsto.eventually` `Filter.tendsto_finset_range` `tendstoUniformlyOn`
`tprod_eq` 📖	mathematical	`HasProdUniformlyOn`	`Set.EqOn` `tprod` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`tprod_eqOn`
`tprod_eqOn` 📖	mathematical	`HasProdUniformlyOn`	`Set.EqOn` `tprod` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`HasProd.tprod_eq` `SummationFilter.instNeBotUnconditional` `hasProd`

HasSumLocallyUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSum` 📖	mathematical	`HasSumLocallyUniformly`	`HasSum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`TendstoLocallyUniformlyOn.tendsto_at` `TendstoLocallyUniformly.tendstoLocallyUniformlyOn` `Set.mem_univ`
`hasSumLocallyUniformlyOn` 📖	mathematical	`HasSumLocallyUniformly`	`HasSumLocallyUniformlyOn`	—	`TendstoLocallyUniformly.tendstoLocallyUniformlyOn`
`summableLocallyUniformly` 📖	mathematical	`HasSumLocallyUniformly`	`SummableLocallyUniformly`	—	—
`tendstoLocallyUniformly_finsetRange` 📖	mathematical	`HasSumLocallyUniformly`	`TendstoLocallyUniformly` `Finset.sum` `Finset.range` `Filter.atTop` `Nat.instPreorder`	—	`tendstoLocallyUniformlyOn_univ` `HasSumLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange` `hasSumLocallyUniformlyOn`

HasSumLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSum` 📖	mathematical	`HasSumLocallyUniformlyOn` `Set` `Set.instMembership`	`HasSum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`TendstoLocallyUniformlyOn.tendsto_at`
`mono` 📖	—	`HasSumLocallyUniformlyOn` `Set` `Set.instHasSubset`	—	—	`TendstoLocallyUniformlyOn.mono`
`summableLocallyUniformlyOn` 📖	mathematical	`HasSumLocallyUniformlyOn`	`SummableLocallyUniformlyOn`	—	—
`tendstoLocallyUniformlyOn_finsetRange` 📖	mathematical	`HasSumLocallyUniformlyOn`	`TendstoLocallyUniformlyOn` `Finset.sum` `Finset.range` `Filter.atTop` `Nat.instPreorder`	—	`hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn` `Filter.Tendsto.eventually` `Filter.tendsto_finset_range`
`tsum_eqOn` 📖	mathematical	`HasSumLocallyUniformlyOn`	`Set.EqOn` `tsum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `SummationFilter.instNeBotUnconditional` `hasSum`

HasSumUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSum` 📖	mathematical	`HasSumUniformly`	`HasSum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`TendstoUniformly.tendsto_at` `tendstoUniformly`
`hasSumLocallyUniformly` 📖	mathematical	`HasSumUniformly`	`HasSumLocallyUniformly`	—	`TendstoUniformly.tendstoLocallyUniformly` `hasSumUniformly_iff_tendstoUniformly`
`hasSumUniformlyOn` 📖	mathematical	`HasSumUniformly`	`HasSumUniformlyOn`	—	`hasSumUniformlyOn_iff_tendstoUniformlyOn` `TendstoUniformly.tendstoUniformlyOn` `tendstoUniformly`
`summableUniformly` 📖	mathematical	`HasSumUniformly`	`SummableUniformly`	—	—
`tendstoUniformly` 📖	mathematical	`HasSumUniformly`	`TendstoUniformly` `Finset` `Finset.sum` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	`hasSumUniformly_iff_tendstoUniformly`
`tendstoUniformlyOn_finsetRange` 📖	mathematical	`HasSumUniformly`	`TendstoUniformly` `Finset.sum` `Finset.range` `Filter.atTop` `Nat.instPreorder`	—	`Filter.Tendsto.eventually` `Filter.tendsto_finset_range` `tendstoUniformly`

HasSumUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_right` 📖	—	`HasSumUniformlyOn` `Set.EqOn`	—	—	`hasSumUniformlyOn_iff_tendstoUniformlyOn` `TendstoUniformlyOn.congr_right` `tendstoUniformlyOn`
`hasSum` 📖	mathematical	`HasSumUniformlyOn` `Set` `Set.instMembership`	`HasSum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`TendstoUniformlyOn.tendsto_at` `tendstoUniformlyOn`
`hasSumLocallyUniformlyOn` 📖	mathematical	`HasSumUniformlyOn`	`HasSumLocallyUniformlyOn`	—	`TendstoUniformlyOn.tendstoLocallyUniformlyOn` `hasSumUniformlyOn_iff_tendstoUniformlyOn`
`mono` 📖	—	`HasSumUniformlyOn` `Set` `Set.instHasSubset`	—	—	`hasSumUniformlyOn_iff_tendstoUniformlyOn` `TendstoUniformlyOn.mono` `tendstoUniformlyOn`
`summableUniformlyOn` 📖	mathematical	`HasSumUniformlyOn`	`SummableUniformlyOn`	—	—
`tendstoUniformlyOn` 📖	mathematical	`HasSumUniformlyOn`	`TendstoUniformlyOn` `Finset` `Finset.sum` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	`hasSumUniformlyOn_iff_tendstoUniformlyOn`
`tendstoUniformlyOn_finsetRange` 📖	mathematical	`HasSumUniformlyOn`	`TendstoUniformlyOn` `Finset.sum` `Finset.range` `Filter.atTop` `Nat.instPreorder`	—	`Filter.Tendsto.eventually` `Filter.tendsto_finset_range` `tendstoUniformlyOn`
`tsum_eq` 📖	mathematical	`HasSumUniformlyOn`	`Set.EqOn` `tsum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`tsum_eqOn`
`tsum_eqOn` 📖	mathematical	`HasSumUniformlyOn`	`Set.EqOn` `tsum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `SummationFilter.instNeBotUnconditional` `hasSum`

MultipliableLocallyUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists` 📖	mathematical	`MultipliableLocallyUniformly`	`HasProdLocallyUniformly`	—	—
`hasProdLocallyUniformly` 📖	mathematical	`MultipliableLocallyUniformly`	`HasProdLocallyUniformly` `tprod` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`TendstoLocallyUniformly.congr_inseparable_right` `tendsto_nhds_unique_inseparable` `instR1Space` `UniformSpace.to_regularSpace` `SummationFilter.instNeBotFinsetFilterOfNeBot` `SummationFilter.instNeBotUnconditional` `HasProdLocallyUniformly.hasProd` `Multipliable.hasProd` `HasProd.multipliable`
`multipliable` 📖	mathematical	`MultipliableLocallyUniformly`	`Multipliable` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`HasProd.multipliable` `HasProdLocallyUniformly.hasProd`
`multipliableLocallyUniformlyOn` 📖	mathematical	`MultipliableLocallyUniformly`	`MultipliableLocallyUniformlyOn`	—	`HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn` `exists` `HasProdLocallyUniformly.hasProdLocallyUniformlyOn`

MultipliableLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_multipliableUniformlyOn` 📖	mathematical	`MultipliableLocallyUniformlyOn` `Set` `Filter` `Filter.instMembership` `nhds`	`nhdsWithin` `MultipliableUniformlyOn`	—	`HasProdLocallyUniformlyOn.exists_hasProdUniformlyOn` `HasProdUniformlyOn.multipliableUniformlyOn`
`hasProdLocallyUniformlyOn` 📖	mathematical	`MultipliableLocallyUniformlyOn`	`HasProdLocallyUniformlyOn` `tprod` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`TendstoLocallyUniformlyOn.congr_inseparable_right` `tendsto_nhds_unique_inseparable` `instR1Space` `UniformSpace.to_regularSpace` `SummationFilter.instNeBotFinsetFilterOfNeBot` `SummationFilter.instNeBotUnconditional` `HasProdLocallyUniformlyOn.hasProd` `Multipliable.hasProd` `HasProd.multipliable`
`mono` 📖	—	`MultipliableLocallyUniformlyOn` `Set` `Set.instHasSubset`	—	—	`HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn` `HasProdLocallyUniformlyOn.mono`
`multipliable` 📖	mathematical	`MultipliableLocallyUniformlyOn` `Set` `Set.instMembership`	`Multipliable` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`HasProd.multipliable` `HasProdLocallyUniformlyOn.hasProd`
`multipliableUniformlyOn_of_isCompact` 📖	mathematical	`MultipliableLocallyUniformlyOn` `IsCompact`	`MultipliableUniformlyOn`	—	`HasProdUniformlyOn.multipliableUniformlyOn` `HasProdLocallyUniformlyOn.hasProdUniformlyOn_of_isCompact`

MultipliableUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists` 📖	mathematical	`MultipliableUniformly`	`HasProdUniformly`	—	—
`hasProdUniformly` 📖	mathematical	`MultipliableUniformly`	`HasProdUniformly` `tprod` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`hasProdUniformlyOn_univ_iff` `MultipliableUniformlyOn.hasProdUniformlyOn` `multipliableUniformlyOn_univ_iff`
`multipliable` 📖	mathematical	`MultipliableUniformly`	`Multipliable` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`HasProd.multipliable` `exists` `HasProdUniformly.hasProd`
`multipliableUniformlyOn` 📖	mathematical	`MultipliableUniformly`	`MultipliableUniformlyOn`	—	`HasProdUniformlyOn.multipliableUniformlyOn` `exists` `HasProdUniformly.hasProdUniformlyOn`

MultipliableUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists` 📖	mathematical	`MultipliableUniformlyOn`	`HasProdUniformlyOn`	—	—
`hasProdUniformlyOn` 📖	mathematical	`MultipliableUniformlyOn`	`HasProdUniformlyOn` `tprod` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`exists` `hasProdUniformlyOn_iff_tendstoUniformlyOn` `TendstoUniformlyOn.congr_inseparable_right` `tendsto_nhds_unique_inseparable` `instR1Space` `UniformSpace.to_regularSpace` `SummationFilter.instNeBotFinsetFilterOfNeBot` `SummationFilter.instNeBotUnconditional` `HasProdUniformlyOn.hasProd` `Multipliable.hasProd` `HasProd.multipliable`
`mono` 📖	—	`MultipliableUniformlyOn` `Set` `Set.instHasSubset`	—	—	`HasProdUniformlyOn.multipliableUniformlyOn` `exists` `HasProdUniformlyOn.mono`
`multipliable` 📖	mathematical	`MultipliableUniformlyOn` `Set` `Set.instMembership`	`Multipliable` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`HasProd.multipliable` `exists` `HasProdUniformlyOn.hasProd`

SummableLocallyUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists` 📖	mathematical	`SummableLocallyUniformly`	`HasSumLocallyUniformly`	—	—
`hasSumLocallyUniformly` 📖	mathematical	`SummableLocallyUniformly`	`HasSumLocallyUniformly` `tsum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`TendstoLocallyUniformly.congr_inseparable_right` `tendsto_nhds_unique_inseparable` `instR1Space` `UniformSpace.to_regularSpace` `SummationFilter.instNeBotFinsetFilterOfNeBot` `SummationFilter.instNeBotUnconditional` `HasSumLocallyUniformly.hasSum` `Summable.hasSum` `HasSum.summable`
`summable` 📖	mathematical	`SummableLocallyUniformly`	`Summable` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`HasSum.summable` `HasSumLocallyUniformly.hasSum`
`summableLocallyUniformlyOn` 📖	mathematical	`SummableLocallyUniformly`	`SummableLocallyUniformlyOn`	—	`HasSumLocallyUniformlyOn.summableLocallyUniformlyOn` `exists` `HasSumLocallyUniformly.hasSumLocallyUniformlyOn`

SummableLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSumLocallyUniformlyOn` 📖	mathematical	`SummableLocallyUniformlyOn`	`HasSumLocallyUniformlyOn` `tsum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`TendstoLocallyUniformlyOn.congr_inseparable_right` `tendsto_nhds_unique_inseparable` `instR1Space` `UniformSpace.to_regularSpace` `SummationFilter.instNeBotFinsetFilterOfNeBot` `SummationFilter.instNeBotUnconditional` `HasSumLocallyUniformlyOn.hasSum` `Summable.hasSum` `HasSum.summable`
`mono` 📖	—	`SummableLocallyUniformlyOn` `Set` `Set.instHasSubset`	—	—	`HasSumLocallyUniformlyOn.summableLocallyUniformlyOn` `HasSumLocallyUniformlyOn.mono`
`summable` 📖	mathematical	`SummableLocallyUniformlyOn` `Set` `Set.instMembership`	`Summable` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`HasSum.summable` `HasSumLocallyUniformlyOn.hasSum`

SummableUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists` 📖	mathematical	`SummableUniformly`	`HasSumUniformly`	—	—
`hasSumUniformly` 📖	mathematical	`SummableUniformly`	`HasSumUniformly` `tsum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`hasSumUniformlyOn_univ_iff` `SummableUniformlyOn.hasSumUniformlyOn` `summableUniformlyOn_univ_iff`
`summable` 📖	mathematical	`SummableUniformly`	`Summable` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`HasSum.summable` `exists` `HasSumUniformly.hasSum`
`summableUniformlyOn` 📖	mathematical	`SummableUniformly`	`SummableUniformlyOn`	—	`HasSumUniformlyOn.summableUniformlyOn` `exists` `HasSumUniformly.hasSumUniformlyOn`

SummableUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists` 📖	mathematical	`SummableUniformlyOn`	`HasSumUniformlyOn`	—	—
`hasSumUniformlyOn` 📖	mathematical	`SummableUniformlyOn`	`HasSumUniformlyOn` `tsum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`exists` `hasSumUniformlyOn_iff_tendstoUniformlyOn` `TendstoUniformlyOn.congr_inseparable_right` `tendsto_nhds_unique_inseparable` `instR1Space` `UniformSpace.to_regularSpace` `SummationFilter.instNeBotFinsetFilterOfNeBot` `SummationFilter.instNeBotUnconditional` `HasSumUniformlyOn.hasSum` `Summable.hasSum` `HasSum.summable`
`mono` 📖	—	`SummableUniformlyOn` `Set` `Set.instHasSubset`	—	—	`HasSumUniformlyOn.summableUniformlyOn` `exists` `HasSumUniformlyOn.mono`
`summable` 📖	mathematical	`SummableUniformlyOn` `Set` `Set.instMembership`	`Summable` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`HasSum.summable` `exists` `HasSumUniformlyOn.hasSum`

(root)

Definitions

Name	Category	Theorems
`HasProdLocallyUniformly` 📖	MathDef	7 math math: `HasProdUniformly.hasProdLocallyUniformly`, `hasProdLocallyUniformly_of_of_forall_exists_nhds`, `hasProdLocallyUniformly_iff_tendstoLocallyUniformly`, `MultipliableLocallyUniformly.hasProdLocallyUniformly`, `MultipliableLocallyUniformly.exists`, `hasProdLocallyUniformly_of_forall_compact`, `multipliableLocallyUniformly_iff_hasProdLocallyUniformly`
`HasProdLocallyUniformlyOn` 📖	MathDef	10 math math: `hasProdLocallyUniformlyOn_of_forall_compact`, `hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn`, `multipliableLocallyUniformlyOn_iff_hasProdLocallyUniformlyOn`, `HasProdLocallyUniformlyOn_euler_sin_prod`, `Summable.hasProdLocallyUniformlyOn_one_add`, `hasProdLocallyUniformlyOn_of_of_forall_exists_nhds`, `HasProdUniformlyOn.hasProdLocallyUniformlyOn`, `Summable.hasProdLocallyUniformlyOn_nat_one_add`, `MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn`, `HasProdLocallyUniformly.hasProdLocallyUniformlyOn`
`HasProdUniformly` 📖	MathDef	5 math math: `multipliableUniformly_iff_hasProdUniformly`, `MultipliableUniformly.exists`, `hasProdUniformlyOn_univ_iff`, `hasProdUniformly_iff_tendstoUniformly`, `MultipliableUniformly.hasProdUniformly`
`HasProdUniformlyOn` 📖	MathDef	12 math math: `MultipliableUniformlyOn.exists`, `MultipliableUniformlyOn.hasProdUniformlyOn`, `HasProdUniformlyOn_sineTerm_prod_on_compact`, `multipliableUniformlyOn_iff_hasProdUniformlyOn`, `HasProdUniformly.hasProdUniformlyOn`, `HasProdLocallyUniformlyOn.exists_hasProdUniformlyOn`, `Summable.hasProdUniformlyOn_nat_one_add`, `hasProdUniformlyOn_univ_iff`, `Summable.hasProdUniformlyOn_one_add`, `hasProdUniformlyOn_iff_tendstoUniformlyOn`, `hasProdUniformlyOn_of_clog`, `HasProdLocallyUniformlyOn.hasProdUniformlyOn_of_isCompact`
`HasSumLocallyUniformly` 📖	MathDef	12 math math: `PeriodPair.hasSumLocallyUniformly_weierstrassP`, `hasSumLocallyUniformly_of_forall_compact`, `HasSumUniformly.hasSumLocallyUniformly`, `PeriodPair.hasSumLocallyUniformly_derivWeierstrassP`, `hasSumLocallyUniformly_of_of_forall_exists_nhds`, `PeriodPair.hasSumLocallyUniformly_weierstrassPExcept`, `PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept`, `PeriodPair.hasSumLocallyUniformly_aux`, `SummableLocallyUniformly.hasSumLocallyUniformly`, `SummableLocallyUniformly.exists`, `hasSumLocallyUniformly_iff_tendstoLocallyUniformly`, `summableLocallyUniformly_iff_hasSumLocallyUniformly`
`HasSumLocallyUniformlyOn` 📖	MathDef	7 math math: `hasSumLocallyUniformlyOn_of_of_forall_exists_nhds`, `hasSumLocallyUniformlyOn_of_forall_compact`, `hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn`, `summableLocallyUniformlyOn_iff_hasSumLocallyUniformlyOn`, `HasSumLocallyUniformly.hasSumLocallyUniformlyOn`, `SummableLocallyUniformlyOn.hasSumLocallyUniformlyOn`, `HasSumUniformlyOn.hasSumLocallyUniformlyOn`
`HasSumUniformly` 📖	MathDef	5 math math: `SummableUniformly.exists`, `hasSumUniformly_iff_tendstoUniformly`, `summableUniformly_iff_hasSumUniformly`, `hasSumUniformlyOn_univ_iff`, `SummableUniformly.hasSumUniformly`
`HasSumUniformlyOn` 📖	MathDef	9 math math: `HasSumUniformly.hasSumUniformlyOn`, `hasSumUniformlyOn_univ_iff`, `summableUniformlyOn_iff_hasSumUniformlyOn`, `SummableUniformlyOn.exists`, `HasSumUniformlyOn.of_norm_le_summable`, `SummableUniformlyOn.hasSumUniformlyOn`, `hasSumUniformlyOn_iff_tendstoUniformlyOn`, `HasSumUniformlyOn.of_norm_le_summable_eventually`, `Summable.hasSumUniformlyOn_log_one_add`
`MultipliableLocallyUniformly` 📖	MathDef	3 math math: `HasProdLocallyUniformly.multipliableLocallyUniformly`, `multipliableLocallyUniformly_of_of_forall_exists_nhds`, `multipliableLocallyUniformly_iff_hasProdLocallyUniformly`
`MultipliableLocallyUniformlyOn` 📖	MathDef	7 math math: `HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn`, `multipliableLocallyUniformlyOn_of_of_forall_exists_nhds`, `multipliableLocallyUniformlyOn_iff_hasProdLocallyUniformlyOn`, `Summable.multipliableLocallyUniformlyOn_one_add`, `Summable.multipliableLocallyUniformlyOn_nat_one_add`, `MultipliableLocallyUniformly.multipliableLocallyUniformlyOn`, `ModularForm.multipliableLocallyUniformlyOn_eta`
`MultipliableUniformly` 📖	MathDef	3 math math: `multipliableUniformly_iff_hasProdUniformly`, `HasProdUniformly.multipliableUniformly`, `multipliableUniformlyOn_univ_iff`
`SummableLocallyUniformly` 📖	MathDef	3 math math: `HasSumLocallyUniformly.summableLocallyUniformly`, `summableLocallyUniformly_of_of_forall_exists_nhds`, `summableLocallyUniformly_iff_hasSumLocallyUniformly`
`SummableLocallyUniformlyOn` 📖	MathDef	9 math math: `summableLocallyUniformlyOn_iteratedDerivWithin_cexp`, `summableLocallyUniformlyOn_of_of_forall_exists_nhds`, `summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm`, `SummableLocallyUniformly.summableLocallyUniformlyOn`, `SummableLocallyUniformlyOn.of_locally_bounded_eventually`, `HasSumLocallyUniformlyOn.summableLocallyUniformlyOn`, `summableLocallyUniformlyOn_iff_hasSumLocallyUniformlyOn`, `SummableLocallyUniformlyOn_of_locally_bounded`, `summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp`
`SummableUniformly` 📖	MathDef	3 math math: `HasSumUniformly.summableUniformly`, `summableUniformly_iff_hasSumUniformly`, `summableUniformlyOn_univ_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`MultipliableLocallyUniformlyOn_congr` 📖	—	`Set.EqOn` `MultipliableLocallyUniformlyOn`	—	—	`HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn` `TendstoLocallyUniformlyOn.congr` `MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn` `eqOn_fun_finsetProd`
`SummableLocallyUniformlyOn_congr` 📖	—	`Set.EqOn` `SummableLocallyUniformlyOn`	—	—	`HasSumLocallyUniformlyOn.summableLocallyUniformlyOn` `TendstoLocallyUniformlyOn.congr` `SummableLocallyUniformlyOn.hasSumLocallyUniformlyOn` `eqOn_fun_finsetSum`
`hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn` 📖	mathematical	—	`HasProdLocallyUniformlyOn` `TendstoLocallyUniformlyOn` `Finset` `Finset.prod` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	—
`hasProdLocallyUniformlyOn_of_forall_compact` 📖	mathematical	`IsOpen` `HasProdUniformlyOn`	`HasProdLocallyUniformlyOn`	—	`HasProdLocallyUniformlyOn.eq_1` `tendstoLocallyUniformlyOn_iff_forall_isCompact`
`hasProdLocallyUniformlyOn_of_of_forall_exists_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `HasProdUniformlyOn`	`HasProdLocallyUniformlyOn`	—	`tendstoLocallyUniformlyOn_of_forall_exists_nhds`
`hasProdLocallyUniformly_iff_tendstoLocallyUniformly` 📖	mathematical	—	`HasProdLocallyUniformly` `TendstoLocallyUniformly` `Finset` `Finset.prod` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	—
`hasProdLocallyUniformly_of_forall_compact` 📖	mathematical	`HasProdUniformlyOn`	`HasProdLocallyUniformly`	—	`HasProdLocallyUniformly.eq_1` `tendstoLocallyUniformly_iff_forall_isCompact`
`hasProdLocallyUniformly_of_of_forall_exists_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `HasProdUniformlyOn`	`HasProdLocallyUniformly`	—	`tendstoLocallyUniformly_of_forall_exists_nhds`
`hasProdUniformlyOn_iff_tendstoUniformlyOn` 📖	mathematical	—	`HasProdUniformlyOn` `TendstoUniformlyOn` `Finset` `Finset.prod` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	`Finset.prod_congr` `Finset.prod_fn` `UniformOnFun.tendsto_iff_tendstoUniformlyOn`
`hasProdUniformlyOn_univ_iff` 📖	mathematical	—	`HasProdUniformlyOn` `Set.univ` `HasProdUniformly`	—	—
`hasProdUniformly_iff_tendstoUniformly` 📖	mathematical	—	`HasProdUniformly` `TendstoUniformly` `Finset` `Finset.prod` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	`Finset.prod_congr` `Finset.prod_fn` `UniformFun.tendsto_iff_tendstoUniformly`
`hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn` 📖	mathematical	—	`HasSumLocallyUniformlyOn` `TendstoLocallyUniformlyOn` `Finset` `Finset.sum` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	—
`hasSumLocallyUniformlyOn_of_forall_compact` 📖	mathematical	`IsOpen` `HasSumUniformlyOn`	`HasSumLocallyUniformlyOn`	—	`HasSumLocallyUniformlyOn.eq_1` `tendstoLocallyUniformlyOn_iff_forall_isCompact` `hasSumUniformlyOn_iff_tendstoUniformlyOn`
`hasSumLocallyUniformlyOn_of_of_forall_exists_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `HasSumUniformlyOn`	`HasSumLocallyUniformlyOn`	—	`tendstoLocallyUniformlyOn_of_forall_exists_nhds` `hasSumUniformlyOn_iff_tendstoUniformlyOn`
`hasSumLocallyUniformly_iff_tendstoLocallyUniformly` 📖	mathematical	—	`HasSumLocallyUniformly` `TendstoLocallyUniformly` `Finset` `Finset.sum` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	—
`hasSumLocallyUniformly_of_forall_compact` 📖	mathematical	`HasSumUniformlyOn`	`HasSumLocallyUniformly`	—	`HasSumLocallyUniformly.eq_1` `tendstoLocallyUniformly_iff_forall_isCompact` `hasSumUniformlyOn_iff_tendstoUniformlyOn`
`hasSumLocallyUniformly_of_of_forall_exists_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `HasSumUniformlyOn`	`HasSumLocallyUniformly`	—	`tendstoLocallyUniformly_of_forall_exists_nhds` `hasSumUniformlyOn_iff_tendstoUniformlyOn`
`hasSumUniformlyOn_iff_tendstoUniformlyOn` 📖	mathematical	—	`HasSumUniformlyOn` `TendstoUniformlyOn` `Finset` `Finset.sum` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	`Finset.sum_congr` `Finset.sum_fn` `Set.mem_singleton_iff` `UniformOnFun.tendsto_iff_tendstoUniformlyOn`
`hasSumUniformlyOn_univ_iff` 📖	mathematical	—	`HasSumUniformlyOn` `Set.univ` `HasSumUniformly`	—	`hasSumUniformlyOn_iff_tendstoUniformlyOn` `tendstoUniformlyOn_univ` `hasSumUniformly_iff_tendstoUniformly`
`hasSumUniformly_iff_tendstoUniformly` 📖	mathematical	—	`HasSumUniformly` `TendstoUniformly` `Finset` `Finset.sum` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	`Finset.sum_congr` `Finset.sum_fn` `UniformFun.tendsto_iff_tendstoUniformly`
`multipliableLocallyUniformlyOn_iff_hasProdLocallyUniformlyOn` 📖	mathematical	—	`MultipliableLocallyUniformlyOn` `HasProdLocallyUniformlyOn` `tprod` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn` `HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn`
`multipliableLocallyUniformlyOn_of_of_forall_exists_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `MultipliableUniformlyOn`	`MultipliableLocallyUniformlyOn`	—	`HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn` `hasProdLocallyUniformlyOn_of_of_forall_exists_nhds` `MultipliableUniformlyOn.hasProdUniformlyOn`
`multipliableLocallyUniformly_iff_hasProdLocallyUniformly` 📖	mathematical	—	`MultipliableLocallyUniformly` `HasProdLocallyUniformly` `tprod` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`MultipliableLocallyUniformly.hasProdLocallyUniformly` `HasProdLocallyUniformly.multipliableLocallyUniformly`
`multipliableLocallyUniformly_of_of_forall_exists_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `MultipliableUniformlyOn`	`MultipliableLocallyUniformly`	—	`HasProdLocallyUniformly.multipliableLocallyUniformly` `hasProdLocallyUniformly_of_of_forall_exists_nhds` `MultipliableUniformlyOn.hasProdUniformlyOn`
`multipliableUniformlyOn_iff_hasProdUniformlyOn` 📖	mathematical	—	`MultipliableUniformlyOn` `HasProdUniformlyOn` `tprod` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`MultipliableUniformlyOn.hasProdUniformlyOn` `HasProdUniformlyOn.multipliableUniformlyOn`
`multipliableUniformlyOn_univ_iff` 📖	mathematical	—	`MultipliableUniformlyOn` `Set.univ` `MultipliableUniformly`	—	`HasProdUniformly.multipliableUniformly` `MultipliableUniformlyOn.exists` `hasProdUniformlyOn_univ_iff` `MultipliableUniformly.multipliableUniformlyOn`
`multipliableUniformly_iff_hasProdUniformly` 📖	mathematical	—	`MultipliableUniformly` `HasProdUniformly` `tprod` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`MultipliableUniformly.hasProdUniformly` `HasProdUniformly.multipliableUniformly`
`summableLocallyUniformlyOn_iff_hasSumLocallyUniformlyOn` 📖	mathematical	—	`SummableLocallyUniformlyOn` `HasSumLocallyUniformlyOn` `tsum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`SummableLocallyUniformlyOn.hasSumLocallyUniformlyOn` `HasSumLocallyUniformlyOn.summableLocallyUniformlyOn`
`summableLocallyUniformlyOn_of_of_forall_exists_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `SummableUniformlyOn`	`SummableLocallyUniformlyOn`	—	`HasSumLocallyUniformlyOn.summableLocallyUniformlyOn` `hasSumLocallyUniformlyOn_of_of_forall_exists_nhds` `SummableUniformlyOn.hasSumUniformlyOn`
`summableLocallyUniformly_iff_hasSumLocallyUniformly` 📖	mathematical	—	`SummableLocallyUniformly` `HasSumLocallyUniformly` `tsum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`SummableLocallyUniformly.hasSumLocallyUniformly` `HasSumLocallyUniformly.summableLocallyUniformly`
`summableLocallyUniformly_of_of_forall_exists_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `SummableUniformlyOn`	`SummableLocallyUniformly`	—	`HasSumLocallyUniformly.summableLocallyUniformly` `hasSumLocallyUniformly_of_of_forall_exists_nhds` `SummableUniformlyOn.hasSumUniformlyOn`
`summableUniformlyOn_iff_hasSumUniformlyOn` 📖	mathematical	—	`SummableUniformlyOn` `HasSumUniformlyOn` `tsum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`SummableUniformlyOn.hasSumUniformlyOn` `HasSumUniformlyOn.summableUniformlyOn`
`summableUniformlyOn_univ_iff` 📖	mathematical	—	`SummableUniformlyOn` `Set.univ` `SummableUniformly`	—	`HasSumUniformly.summableUniformly` `SummableUniformlyOn.exists` `hasSumUniformlyOn_univ_iff` `SummableUniformly.summableUniformlyOn`
`summableUniformly_iff_hasSumUniformly` 📖	mathematical	—	`SummableUniformly` `HasSumUniformly` `tsum` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	`SummableUniformly.hasSumUniformly` `HasSumUniformly.summableUniformly`

---

← Back to Index