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 📖	—	TendstoLocallyUniformly Filter.Frequently Continuous UniformSpace.toTopologicalSpace	—	—	continuousOn_univ TendstoLocallyUniformlyOn.continuousOn tendstoLocallyUniformlyOn Filter.Frequently.mono Continuous.continuousOn
tendsto_comp 📖	—	TendstoLocallyUniformly ContinuousAt UniformSpace.toTopologicalSpace Filter.Tendsto nhds	—	—	tendsto_comp_of_locally_uniform_limit

TendstoLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn 📖	—	TendstoLocallyUniformlyOn Filter.Frequently 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	nhds	—	tendsto_comp_of_locally_uniform_limit_within

TendstoUniformly

Theorems

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

TendstoUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn 📖	—	TendstoUniformlyOn Filter.Frequently ContinuousOn UniformSpace.toTopologicalSpace	—	—	TendstoLocallyUniformlyOn.continuousOn tendstoLocallyUniformlyOn
tendsto_comp 📖	mathematical	TendstoUniformlyOn ContinuousWithinAt UniformSpace.toTopologicalSpace Filter.Tendsto nhdsWithin	nhds	—	tendsto_comp_of_locally_uniform_limit_within self_mem_nhdsWithin
uniformContinuousOn 📖	—	TendstoUniformlyOn Filter.Frequently 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 📖	—	Set Filter Filter.instMembership nhds ContinuousAt UniformSpace.toTopologicalSpace Set.instMembership	—	—	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	—	continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt
continuousOn_of_uniform_approx_of_continuousOn 📖	—	ContinuousOn UniformSpace.toTopologicalSpace Set Set.instMembership	—	—	continuousOn_of_locally_uniform_approx_of_continuousWithinAt self_mem_nhdsWithin ContinuousOn.continuousWithinAt
continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt 📖	—	Set Set.instMembership Filter Filter.instMembership nhdsWithin 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	—	continuous_iff_continuousAt continuousAt_of_locally_uniform_approx_of_continuousAt
continuous_of_uniform_approx_of_continuous 📖	—	Continuous UniformSpace.toTopologicalSpace Set Set.instMembership	—	—	continuousOn_univ continuousOn_of_uniform_approx_of_continuousOn
tendsto_comp_of_locally_uniform_limit 📖	—	ContinuousAt UniformSpace.toTopologicalSpace Filter.Tendsto nhds Set Filter Filter.instMembership Filter.Eventually	—	—	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	nhds	—	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 📖	—	UniformContinuousOn Set Set.instMembership	—	—	comp_comp_symm_mem_uniformity_sets Filter.mp_mem Filter.univ_mem' SetRel.prodMk_mem_comp Subtype.prop
uniformContinuous_of_uniform_approx_of_uniformContinuous 📖	—	UniformContinuous Set Set.instMembership	—	—	uniformContinuousOn_univ uniformContinuousOn_of_uniform_approx_of_uniformContinuousOn

---

← Back to Index