Documentation Verification Report

UniformApproximation

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

Statistics

Metric	Count
Definitions	0
Theorems `continuous`, `tendsto_comp`, `continuousOn`, `tendsto_comp`, `continuous`, `tendsto_comp`, `uniformContinuous`, `continuousOn`, `tendsto_comp`, `uniformContinuousOn`, `continuousAt_of_locally_uniform_approx_of_continuousAt`, `continuousOn_of_locally_uniform_approx_of_continuousWithinAt`, `continuousOn_of_uniform_approx_of_continuousOn`, `continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt`, `continuous_of_locally_uniform_approx_of_continuousAt`, `continuous_of_uniform_approx_of_continuous`, `tendsto_comp_of_locally_uniform_limit`, `tendsto_comp_of_locally_uniform_limit_within`, `uniformContinuousOn_of_uniform_approx_of_uniformContinuousOn`, `uniformContinuous_of_uniform_approx_of_uniformContinuous`	20
Total	20

TendstoLocallyUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous` 📖	mathematical	`TendstoLocallyUniformly` `Filter.Frequently` `Continuous` `UniformSpace.toTopologicalSpace`	`Continuous` `UniformSpace.toTopologicalSpace`	—	`continuousOn_univ` `TendstoLocallyUniformlyOn.continuousOn` `tendstoLocallyUniformlyOn` `Filter.Frequently.mono` `Continuous.continuousOn`
`tendsto_comp` 📖	mathematical	`TendstoLocallyUniformly` `ContinuousAt` `UniformSpace.toTopologicalSpace` `Filter.Tendsto` `nhds`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	—	`tendsto_comp_of_locally_uniform_limit`

TendstoLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn` 📖	mathematical	`TendstoLocallyUniformlyOn` `Filter.Frequently` `ContinuousOn` `UniformSpace.toTopologicalSpace`	`ContinuousOn` `UniformSpace.toTopologicalSpace`	—	`continuousOn_of_locally_uniform_approx_of_continuousWithinAt` `Filter.Frequently.exists` `Filter.Frequently.and_eventually` `ContinuousOn.continuousWithinAt`
`tendsto_comp` 📖	mathematical	`TendstoLocallyUniformlyOn` `ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `Set` `Set.instMembership` `Filter.Tendsto` `nhdsWithin`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	—	`tendsto_comp_of_locally_uniform_limit_within`

TendstoUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous` 📖	mathematical	`TendstoUniformly` `Filter.Frequently` `Continuous` `UniformSpace.toTopologicalSpace`	`Continuous` `UniformSpace.toTopologicalSpace`	—	`TendstoLocallyUniformly.continuous` `tendstoLocallyUniformly`
`tendsto_comp` 📖	mathematical	`TendstoUniformly` `ContinuousAt` `UniformSpace.toTopologicalSpace` `Filter.Tendsto` `nhds`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	—	`TendstoLocallyUniformly.tendsto_comp` `tendstoLocallyUniformly`
`uniformContinuous` 📖	mathematical	`TendstoUniformly` `Filter.Frequently` `UniformContinuous`	`UniformContinuous`	—	`uniformContinuous_of_uniform_approx_of_uniformContinuous` `Filter.Frequently.exists` `Filter.Frequently.and_eventually`

TendstoUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn` 📖	mathematical	`TendstoUniformlyOn` `Filter.Frequently` `ContinuousOn` `UniformSpace.toTopologicalSpace`	`ContinuousOn` `UniformSpace.toTopologicalSpace`	—	`TendstoLocallyUniformlyOn.continuousOn` `tendstoLocallyUniformlyOn`
`tendsto_comp` 📖	mathematical	`TendstoUniformlyOn` `ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `Filter.Tendsto` `nhdsWithin`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	—	`tendsto_comp_of_locally_uniform_limit_within` `self_mem_nhdsWithin`
`uniformContinuousOn` 📖	mathematical	`TendstoUniformlyOn` `Filter.Frequently` `UniformContinuousOn`	`UniformContinuousOn`	—	`uniformContinuousOn_of_uniform_approx_of_uniformContinuousOn` `Filter.Frequently.exists` `Filter.Frequently.and_eventually`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_of_locally_uniform_approx_of_continuousAt` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `ContinuousAt` `UniformSpace.toTopologicalSpace` `Set.instMembership`	`ContinuousAt` `UniformSpace.toTopologicalSpace`	—	`continuousWithinAt_univ` `continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt` `Set.mem_univ` `nhdsWithin_univ`
`continuousOn_of_locally_uniform_approx_of_continuousWithinAt` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `Set.instMembership`	`ContinuousOn` `UniformSpace.toTopologicalSpace`	—	`continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt`
`continuousOn_of_uniform_approx_of_continuousOn` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `Set` `Set.instMembership`	`ContinuousOn` `UniformSpace.toTopologicalSpace`	—	`continuousOn_of_locally_uniform_approx_of_continuousWithinAt` `self_mem_nhdsWithin` `ContinuousOn.continuousWithinAt`
`continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt` 📖	mathematical	`Set` `Set.instMembership` `Filter` `Filter.instMembership` `nhdsWithin` `ContinuousWithinAt` `UniformSpace.toTopologicalSpace`	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace`	—	`Uniform.continuousWithinAt_iff'_left` `comp_mem_uniformity_sets` `comp_symm_of_uniformity` `Filter.Eventually.mono` `Filter.Eventually.and` `SetRel.prodMk_mem_comp` `refl_mem_uniformity` `Filter.Eventually.self_of_nhdsWithin`
`continuous_of_locally_uniform_approx_of_continuousAt` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `ContinuousAt` `UniformSpace.toTopologicalSpace` `Set.instMembership`	`Continuous` `UniformSpace.toTopologicalSpace`	—	`continuous_iff_continuousAt` `continuousAt_of_locally_uniform_approx_of_continuousAt`
`continuous_of_uniform_approx_of_continuous` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `Set` `Set.instMembership`	`Continuous` `UniformSpace.toTopologicalSpace`	—	`continuousOn_univ` `continuousOn_of_uniform_approx_of_continuousOn`
`tendsto_comp_of_locally_uniform_limit` 📖	mathematical	`ContinuousAt` `UniformSpace.toTopologicalSpace` `Filter.Tendsto` `nhds` `Set` `Filter` `Filter.instMembership` `Filter.Eventually`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	—	`tendsto_comp_of_locally_uniform_limit_within` `continuousWithinAt_univ` `nhdsWithin_univ`
`tendsto_comp_of_locally_uniform_limit_within` 📖	mathematical	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `Filter.Tendsto` `nhdsWithin` `Set` `Filter` `Filter.instMembership` `Filter.Eventually`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace`	—	`Uniform.tendsto_nhds_right` `comp_mem_uniformity_sets` `Uniform.continuousWithinAt_iff'_right` `Filter.Eventually.mp` `Filter.Eventually.mono` `SetRel.prodMk_mem_comp`
`uniformContinuousOn_of_uniform_approx_of_uniformContinuousOn` 📖	mathematical	`UniformContinuousOn` `Set` `Set.instMembership`	`UniformContinuousOn`	—	`comp_comp_symm_mem_uniformity_sets` `Filter.mp_mem` `Filter.univ_mem'` `SetRel.prodMk_mem_comp` `Subtype.prop`
`uniformContinuous_of_uniform_approx_of_uniformContinuous` 📖	mathematical	`UniformContinuous` `Set` `Set.instMembership`	`UniformContinuous`	—	`uniformContinuousOn_univ` `uniformContinuousOn_of_uniform_approx_of_uniformContinuousOn`

---

← Back to Index