Equicontinuity

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

Statistics

Metric	Count
Definitions Equicontinuous, EquicontinuousAt, EquicontinuousOn, EquicontinuousWithinAt, Equicontinuous, EquicontinuousAt, EquicontinuousOn, EquicontinuousWithinAt, UniformEquicontinuous, UniformEquicontinuousOn, UniformEquicontinuous, UniformEquicontinuousOn	12
Theorems closure', comp, continuous, equicontinuousOn, isClosed_setOf_tendsto, closure', comp, continuousAt, equicontinuousWithinAt, tendsto_of_mem_closure, closure', comp, continuousOn, mono, closure', comp, continuousWithinAt, mono, equicontinuousAt_iff, equicontinuousAt_iff_left, equicontinuousAt_iff_right, equicontinuousWithinAt_iff, equicontinuousWithinAt_iff_left, equicontinuousWithinAt_iff_right, uniformEquicontinuousOn_iff, uniformEquicontinuousOn_iff_left, uniformEquicontinuousOn_iff_right, uniformEquicontinuous_iff, uniformEquicontinuous_iff_left, uniformEquicontinuous_iff_right, continuousAt_of_equicontinuousAt, continuousOn_of_equicontinuousOn, continuousWithinAt_of_equicontinuousWithinAt, continuous_of_equicontinuous, uniformContinuousOn_of_uniformEquicontinuousOn, uniformContinuous_of_uniformEquicontinuous, equicontinuousAt_iff, equicontinuousOn_iff, equicontinuousWithinAt_iff, equicontinuous_iff, uniformEquicontinuousOn_iff, uniformEquicontinuous_iff, closure, continuous_of_mem, mono, closure, continuousAt_of_mem, mono, closure, continuousOn_of_mem, mono, closure, continuousWithinAt_of_mem, mono, closure, mono, uniformContinuous_of_mem, closure, mono, uniformContinuousOn_of_mem, closure', comp, equicontinuous, uniformContinuous, uniformEquicontinuousOn, closure', comp, equicontinuousOn, mono, uniformContinuousOn, equicontinuousAt_empty, equicontinuousAt_finite, equicontinuousAt_iInf_dom, equicontinuousAt_iInf_rng, equicontinuousAt_iff_continuousAt, equicontinuousAt_iff_pair, equicontinuousAt_iff_range, equicontinuousAt_restrict_iff, equicontinuousAt_unique, equicontinuousOn_empty, equicontinuousOn_finite, equicontinuousOn_iInf_dom, equicontinuousOn_iInf_rng, equicontinuousOn_iff_continuousOn, equicontinuousOn_iff_range, equicontinuousOn_unique, equicontinuousOn_univ, equicontinuousWithinAt_empty, equicontinuousWithinAt_finite, equicontinuousWithinAt_iInf_dom, equicontinuousWithinAt_iInf_rng, equicontinuousWithinAt_iff_continuousWithinAt, equicontinuousWithinAt_iff_pair, equicontinuousWithinAt_iff_range, equicontinuousWithinAt_unique, equicontinuousWithinAt_univ, equicontinuous_empty, equicontinuous_finite, equicontinuous_iInf_dom, equicontinuous_iInf_rng, equicontinuous_iff_continuous, equicontinuous_iff_range, equicontinuous_restrict_iff, equicontinuous_unique, uniformEquicontinuousOn_empty, uniformEquicontinuousOn_finite, uniformEquicontinuousOn_iInf_dom, uniformEquicontinuousOn_iInf_rng, uniformEquicontinuousOn_iff_range, uniformEquicontinuousOn_iff_uniformContinuousOn, uniformEquicontinuousOn_unique, uniformEquicontinuousOn_univ, uniformEquicontinuous_empty, uniformEquicontinuous_finite, uniformEquicontinuous_iInf_dom, uniformEquicontinuous_iInf_rng, uniformEquicontinuous_iff_range, uniformEquicontinuous_iff_uniformContinuous, uniformEquicontinuous_restrict_iff, uniformEquicontinuous_unique	120
Total	132

Equicontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure' 📖	mathematical	Equicontinuous Set.Elem Set Set.instMembership Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace	closure	—	EquicontinuousAt.closure'
comp 📖	—	Equicontinuous	—	—	EquicontinuousAt.comp
continuous 📖	mathematical	Equicontinuous	Continuous UniformSpace.toTopologicalSpace	—	continuous_iff_continuousAt EquicontinuousAt.continuousAt
equicontinuousOn 📖	mathematical	Equicontinuous	EquicontinuousOn	—	EquicontinuousAt.equicontinuousWithinAt
isClosed_setOf_tendsto 📖	mathematical	Equicontinuous Continuous UniformSpace.toTopologicalSpace	IsClosed setOf Filter.Tendsto nhds	—	closure_subset_iff_isClosed EquicontinuousAt.tendsto_of_mem_closure Filter.Tendsto.mono_left Continuous.continuousAt inf_le_left

EquicontinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure' 📖	mathematical	EquicontinuousAt Set.Elem Set Set.instMembership Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace	closure	—	equicontinuousWithinAt_univ EquicontinuousWithinAt.closure' Continuous.comp Pi.continuous_restrict continuous_apply
comp 📖	—	EquicontinuousAt	—	—	Filter.Eventually.mono
continuousAt 📖	mathematical	EquicontinuousAt	ContinuousAt UniformSpace.toTopologicalSpace	—	Filter.HasBasis.tendsto_right_iff UniformSpace.hasBasis_nhds Filter.Eventually.mono
equicontinuousWithinAt 📖	mathematical	EquicontinuousAt	EquicontinuousWithinAt	—	Filter.Eventually.filter_mono inf_le_left
tendsto_of_mem_closure 📖	—	EquicontinuousAt Filter.Tendsto nhdsWithin nhds UniformSpace.toTopologicalSpace Set Set.instMembership closure	—	—	Filter.HasBasis.tendsto_right_iff nhds_basis_uniformity Filter.basis_sets comp_comp_symm_mem_uniformity_sets Filter.Eventually.and eventually_mem_nhdsWithin Filter.Eventually.filter_mono nhdsWithin_le_nhds Filter.Eventually.exists mem_closure_iff_nhdsWithin_neBot Filter.mp_mem UniformSpace.ball_mem_nhds Filter.univ_mem' UniformSpace.mem_ball_symmetry

EquicontinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure' 📖	mathematical	EquicontinuousOn Set.Elem Set Set.instMembership Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace Set.restrict	closure	—	EquicontinuousWithinAt.closure' Continuous.comp continuous_apply
comp 📖	—	EquicontinuousOn	—	—	EquicontinuousWithinAt.comp
continuousOn 📖	mathematical	EquicontinuousOn	ContinuousOn UniformSpace.toTopologicalSpace	—	EquicontinuousWithinAt.continuousWithinAt
mono 📖	—	EquicontinuousOn Set Set.instHasSubset	—	—	EquicontinuousWithinAt.mono

EquicontinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure' 📖	mathematical	EquicontinuousWithinAt Set.Elem Set Set.instMembership Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace Set.restrict Function.eval	closure	—	mem_uniformity_isClosed Filter.mp_mem eventually_mem_nhdsWithin Filter.univ_mem' SetCoe.forall HasSubset.Subset.trans Set.instIsTransSubset closure_minimal IsClosed.preimage Continuous.prodMk Continuous.comp continuous_apply Set.preimage_mono
comp 📖	—	EquicontinuousWithinAt	—	—	Filter.Eventually.mono
continuousWithinAt 📖	mathematical	EquicontinuousWithinAt	ContinuousWithinAt UniformSpace.toTopologicalSpace	—	Filter.HasBasis.tendsto_right_iff UniformSpace.hasBasis_nhds Filter.Eventually.mono
mono 📖	—	EquicontinuousWithinAt Set Set.instHasSubset	—	—	Filter.Eventually.filter_mono nhdsWithin_mono

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equicontinuousAt_iff 📖	mathematical	Filter.HasBasis nhds uniformity	EquicontinuousAt Set Set.instMembership	—	equicontinuousAt_iff_continuousAt ContinuousAt.eq_1 tendsto_iff UniformFun.hasBasis_nhds_of_basis
equicontinuousAt_iff_left 📖	mathematical	Filter.HasBasis nhds	EquicontinuousAt Set Set.instMembership	—	equicontinuousAt_iff_continuousAt ContinuousAt.eq_1 tendsto_iff UniformFun.hasBasis_nhds
equicontinuousAt_iff_right 📖	mathematical	Filter.HasBasis uniformity	EquicontinuousAt Filter.Eventually nhds	—	equicontinuousAt_iff_continuousAt ContinuousAt.eq_1 tendsto_right_iff UniformFun.hasBasis_nhds_of_basis
equicontinuousWithinAt_iff 📖	mathematical	Filter.HasBasis nhdsWithin uniformity	EquicontinuousWithinAt Set Set.instMembership	—	equicontinuousWithinAt_iff_continuousWithinAt ContinuousWithinAt.eq_1 tendsto_iff UniformFun.hasBasis_nhds_of_basis
equicontinuousWithinAt_iff_left 📖	mathematical	Filter.HasBasis nhdsWithin	EquicontinuousWithinAt Set Set.instMembership	—	equicontinuousWithinAt_iff_continuousWithinAt ContinuousWithinAt.eq_1 tendsto_iff UniformFun.hasBasis_nhds
equicontinuousWithinAt_iff_right 📖	mathematical	Filter.HasBasis uniformity	EquicontinuousWithinAt Filter.Eventually nhdsWithin	—	equicontinuousWithinAt_iff_continuousWithinAt ContinuousWithinAt.eq_1 tendsto_right_iff UniformFun.hasBasis_nhds_of_basis
uniformEquicontinuousOn_iff 📖	mathematical	Filter.HasBasis Filter Filter.instInf uniformity Filter.principal SProd.sprod Set Set.instSProd	UniformEquicontinuousOn Set.instMembership	—	uniformEquicontinuousOn_iff_uniformContinuousOn UniformContinuousOn.eq_1 tendsto_iff UniformFun.hasBasis_uniformity_of_basis
uniformEquicontinuousOn_iff_left 📖	mathematical	Filter.HasBasis Filter Filter.instInf uniformity Filter.principal SProd.sprod Set Set.instSProd	UniformEquicontinuousOn Set.instMembership	—	uniformEquicontinuousOn_iff_uniformContinuousOn UniformContinuousOn.eq_1 tendsto_iff UniformFun.hasBasis_uniformity
uniformEquicontinuousOn_iff_right 📖	mathematical	Filter.HasBasis uniformity	UniformEquicontinuousOn Filter.Eventually Filter Filter.instInf Filter.principal SProd.sprod Set Set.instSProd	—	uniformEquicontinuousOn_iff_uniformContinuousOn UniformContinuousOn.eq_1 tendsto_right_iff UniformFun.hasBasis_uniformity_of_basis
uniformEquicontinuous_iff 📖	mathematical	Filter.HasBasis uniformity	UniformEquicontinuous Set Set.instMembership	—	uniformEquicontinuous_iff_uniformContinuous UniformContinuous.eq_1 tendsto_iff UniformFun.hasBasis_uniformity_of_basis
uniformEquicontinuous_iff_left 📖	mathematical	Filter.HasBasis uniformity	UniformEquicontinuous Set Set.instMembership	—	uniformEquicontinuous_iff_uniformContinuous UniformContinuous.eq_1 tendsto_iff UniformFun.hasBasis_uniformity
uniformEquicontinuous_iff_right 📖	mathematical	Filter.HasBasis uniformity	UniformEquicontinuous Filter.Eventually	—	uniformEquicontinuous_iff_uniformContinuous UniformContinuous.eq_1 tendsto_right_iff UniformFun.hasBasis_uniformity_of_basis

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt_of_equicontinuousAt 📖	mathematical	Filter.Tendsto nhds Pi.topologicalSpace UniformSpace.toTopologicalSpace EquicontinuousAt	ContinuousAt	—	continuousWithinAt_univ continuousWithinAt_of_equicontinuousWithinAt tendsto_pi_nhds equicontinuousWithinAt_univ
continuousOn_of_equicontinuousOn 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace EquicontinuousOn	ContinuousOn	—	continuousWithinAt_of_equicontinuousWithinAt
continuousWithinAt_of_equicontinuousWithinAt 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace EquicontinuousWithinAt	ContinuousWithinAt	—	Filter.mem_map UniformSpace.mem_nhds_iff mem_uniformity_isClosed Filter.mp_mem eventually_mem_nhdsWithin Filter.univ_mem' UniformSpace.ball_mono IsClosed.mem_of_tendsto prodMk_nhds Filter.Eventually.of_forall
continuous_of_equicontinuous 📖	mathematical	Filter.Tendsto nhds Pi.topologicalSpace UniformSpace.toTopologicalSpace Equicontinuous	Continuous	—	continuous_iff_continuousAt continuousAt_of_equicontinuousAt
uniformContinuousOn_of_uniformEquicontinuousOn 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace UniformEquicontinuousOn	UniformContinuousOn	—	Filter.mem_map mem_uniformity_isClosed Filter.mp_mem Filter.mem_inf_of_right Filter.mem_principal_self Filter.univ_mem' IsClosed.mem_of_tendsto prodMk_nhds Filter.Eventually.of_forall
uniformContinuous_of_uniformEquicontinuous 📖	mathematical	Filter.Tendsto nhds Pi.topologicalSpace UniformSpace.toTopologicalSpace UniformEquicontinuous	UniformContinuous	—	uniformContinuousOn_univ uniformContinuousOn_of_uniformEquicontinuousOn tendsto_pi_nhds uniformEquicontinuousOn_univ

IsUniformInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equicontinuousAt_iff 📖	mathematical	IsUniformInducing	EquicontinuousAt	—	isInducing UniformFun.postcomp_isUniformInducing equicontinuousAt_iff_continuousAt Topology.IsInducing.continuousAt_iff
equicontinuousOn_iff 📖	mathematical	IsUniformInducing	EquicontinuousOn	—	equicontinuousWithinAt_iff
equicontinuousWithinAt_iff 📖	mathematical	IsUniformInducing	EquicontinuousWithinAt	—	isInducing UniformFun.postcomp_isUniformInducing Topology.IsInducing.continuousWithinAt_iff
equicontinuous_iff 📖	mathematical	IsUniformInducing	Equicontinuous	—	equicontinuousAt_iff
uniformEquicontinuousOn_iff 📖	mathematical	IsUniformInducing	UniformEquicontinuousOn	—	UniformFun.postcomp_isUniformInducing uniformContinuousOn_iff
uniformEquicontinuous_iff 📖	mathematical	IsUniformInducing	UniformEquicontinuous	—	UniformFun.postcomp_isUniformInducing uniformContinuous_iff

Set

Definitions

Name	Category	Theorems
Equicontinuous 📖	MathDef	—
EquicontinuousAt 📖	MathDef	—
EquicontinuousOn 📖	MathDef	—
EquicontinuousWithinAt 📖	MathDef	—
UniformEquicontinuous 📖	MathDef	—
UniformEquicontinuousOn 📖	MathDef	—

Set.Equicontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	Set.Equicontinuous	closure Pi.topologicalSpace UniformSpace.toTopologicalSpace	—	Set.EquicontinuousAt.closure
continuous_of_mem 📖	mathematical	Set.Equicontinuous Set Set.instMembership	Continuous UniformSpace.toTopologicalSpace	—	Equicontinuous.continuous
mono 📖	—	Set.Equicontinuous Set Set.instHasSubset	—	—	Equicontinuous.comp

Set.EquicontinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	Set.EquicontinuousAt	closure Pi.topologicalSpace UniformSpace.toTopologicalSpace	—	EquicontinuousAt.closure' continuous_id
continuousAt_of_mem 📖	mathematical	Set.EquicontinuousAt Set Set.instMembership	ContinuousAt UniformSpace.toTopologicalSpace	—	EquicontinuousAt.continuousAt
mono 📖	—	Set.EquicontinuousAt Set Set.instHasSubset	—	—	EquicontinuousAt.comp

Set.EquicontinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	Set.EquicontinuousOn	closure Pi.topologicalSpace UniformSpace.toTopologicalSpace	—	Set.EquicontinuousWithinAt.closure
continuousOn_of_mem 📖	mathematical	Set.EquicontinuousOn Set Set.instMembership	ContinuousOn UniformSpace.toTopologicalSpace	—	EquicontinuousOn.continuousOn
mono 📖	—	Set.EquicontinuousOn Set Set.instHasSubset	—	—	EquicontinuousOn.comp

Set.EquicontinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	Set.EquicontinuousWithinAt	closure Pi.topologicalSpace UniformSpace.toTopologicalSpace	—	EquicontinuousWithinAt.closure' Pi.continuous_restrict continuous_apply
continuousWithinAt_of_mem 📖	mathematical	Set.EquicontinuousWithinAt Set Set.instMembership	ContinuousWithinAt UniformSpace.toTopologicalSpace	—	EquicontinuousWithinAt.continuousWithinAt
mono 📖	—	Set.EquicontinuousWithinAt Set Set.instHasSubset	—	—	EquicontinuousWithinAt.comp

Set.UniformEquicontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	Set.UniformEquicontinuous	closure Pi.topologicalSpace UniformSpace.toTopologicalSpace	—	UniformEquicontinuous.closure' continuous_id
mono 📖	—	Set.UniformEquicontinuous Set Set.instHasSubset	—	—	UniformEquicontinuous.comp
uniformContinuous_of_mem 📖	mathematical	Set.UniformEquicontinuous Set Set.instMembership	UniformContinuous	—	UniformEquicontinuous.uniformContinuous

Set.UniformEquicontinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	Set.UniformEquicontinuousOn	closure Pi.topologicalSpace UniformSpace.toTopologicalSpace	—	UniformEquicontinuousOn.closure' Pi.continuous_restrict
mono 📖	—	Set.UniformEquicontinuousOn Set Set.instHasSubset	—	—	UniformEquicontinuousOn.comp
uniformContinuousOn_of_mem 📖	mathematical	Set.UniformEquicontinuousOn Set Set.instMembership	UniformContinuousOn	—	UniformEquicontinuousOn.uniformContinuousOn

UniformEquicontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure' 📖	mathematical	UniformEquicontinuous Set.Elem Set Set.instMembership Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace	closure	—	uniformEquicontinuousOn_univ UniformEquicontinuousOn.closure' Continuous.comp Pi.continuous_restrict
comp 📖	—	UniformEquicontinuous	—	—	Filter.Eventually.mono
equicontinuous 📖	mathematical	UniformEquicontinuous	Equicontinuous UniformSpace.toTopologicalSpace	—	Filter.mem_of_superset UniformSpace.ball_mem_nhds
uniformContinuous 📖	mathematical	UniformEquicontinuous	UniformContinuous	—	Filter.mem_map Filter.mem_of_superset
uniformEquicontinuousOn 📖	mathematical	UniformEquicontinuous	UniformEquicontinuousOn	—	Filter.Eventually.filter_mono inf_le_left

UniformEquicontinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure' 📖	mathematical	UniformEquicontinuousOn Set.Elem Set Set.instMembership Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace Set.restrict	closure	—	mem_uniformity_isClosed Filter.mp_mem Filter.mem_inf_of_right Filter.mem_principal_self Filter.univ_mem' SetCoe.forall HasSubset.Subset.trans Set.instIsTransSubset closure_minimal IsClosed.preimage Continuous.prodMk Continuous.comp continuous_apply Set.preimage_mono
comp 📖	—	UniformEquicontinuousOn	—	—	Filter.Eventually.mono
equicontinuousOn 📖	mathematical	UniformEquicontinuousOn	EquicontinuousOn UniformSpace.toTopologicalSpace	—	Filter.mem_of_superset UniformSpace.ball_mem_nhdsWithin
mono 📖	—	UniformEquicontinuousOn Set Set.instHasSubset	—	—	Filter.Eventually.filter_mono inf_le_inf le_refl Set.prod_mono
uniformContinuousOn 📖	mathematical	UniformEquicontinuousOn	UniformContinuousOn	—	Filter.mem_map Filter.mem_of_superset

(root)

Definitions

Name	Category	Theorems
Equicontinuous 📖	MathDef	15 math math: equicontinuous_restrict_iff, equicontinuous_iInf_rng, equicontinuous_finite, UniformEquicontinuous.equicontinuous, Metric.equicontinuous_of_continuity_modulus, equicontinuous_iff_range, NormedSpace.equicontinuous_TFAE, equicontinuous_iff_continuous, WithSeminorms.equicontinuous_TFAE, equicontinuous_unique, equicontinuousOn_univ, equicontinuous_of_equicontinuousAt_one, equicontinuous_of_equicontinuousAt_zero, equicontinuous_empty, IsUniformInducing.equicontinuous_iff
EquicontinuousAt 📖	MathDef	19 math math: Metric.equicontinuousAt_iff_right, Metric.equicontinuousAt_iff_pair, equicontinuousAt_empty, IsUniformInducing.equicontinuousAt_iff, Metric.equicontinuousAt_iff, Filter.HasBasis.equicontinuousAt_iff_left, Filter.HasBasis.equicontinuousAt_iff_right, Filter.HasBasis.equicontinuousAt_iff, equicontinuousAt_iff_range, Metric.equicontinuousAt_of_continuity_modulus, NormedSpace.equicontinuous_TFAE, WithSeminorms.equicontinuous_TFAE, equicontinuousWithinAt_univ, equicontinuousAt_iff_pair, equicontinuousAt_restrict_iff, equicontinuousAt_iff_continuousAt, equicontinuousAt_finite, equicontinuousAt_iInf_rng, equicontinuousAt_unique
EquicontinuousOn 📖	MathDef	11 math math: equicontinuous_restrict_iff, equicontinuousOn_iff_continuousOn, equicontinuousOn_empty, Equicontinuous.equicontinuousOn, equicontinuousOn_iff_range, equicontinuousOn_iInf_rng, IsUniformInducing.equicontinuousOn_iff, equicontinuousOn_unique, equicontinuousOn_univ, UniformEquicontinuousOn.equicontinuousOn, equicontinuousOn_finite
EquicontinuousWithinAt 📖	MathDef	14 math math: equicontinuousWithinAt_iff_pair, equicontinuousWithinAt_empty, equicontinuousWithinAt_iff_continuousWithinAt, Filter.HasBasis.equicontinuousWithinAt_iff_right, Filter.HasBasis.equicontinuousWithinAt_iff, equicontinuousWithinAt_unique, equicontinuousWithinAt_univ, equicontinuousWithinAt_iff_range, equicontinuousWithinAt_finite, Filter.HasBasis.equicontinuousWithinAt_iff_left, equicontinuousAt_restrict_iff, equicontinuousWithinAt_iInf_rng, EquicontinuousAt.equicontinuousWithinAt, IsUniformInducing.equicontinuousWithinAt_iff
UniformEquicontinuous 📖	MathDef	26 math math: WithSeminorms.banach_steinhaus, uniformEquicontinuousOn_univ, uniformEquicontinuous_restrict_iff, IsUniformInducing.uniformEquicontinuous_iff, Metric.uniformEquicontinuous_iff, WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm, uniformEquicontinuous_iInf_rng, uniformEquicontinuous_empty, Filter.HasBasis.uniformEquicontinuous_iff_right, uniformEquicontinuous_unique, WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup, Filter.HasBasis.uniformEquicontinuous_iff, NormedSpace.equicontinuous_TFAE, WithSeminorms.equicontinuous_TFAE, LipschitzWith.uniformEquicontinuous, Filter.HasBasis.uniformEquicontinuous_iff_left, Metric.uniformEquicontinuous_iff_right, PolynormableSpace.banach_steinhaus, uniformEquicontinuous_of_equicontinuousAt_zero, uniformEquicontinuous_iff_range, uniformEquicontinuous_birkhoffAverage, uniformEquicontinuous_of_equicontinuousAt_one, CompactSpace.uniformEquicontinuous_of_equicontinuous, Metric.uniformEquicontinuous_of_continuity_modulus, uniformEquicontinuous_finite, uniformEquicontinuous_iff_uniformContinuous
UniformEquicontinuousOn 📖	MathDef	14 math math: uniformEquicontinuousOn_univ, LipschitzOnWith.uniformEquicontinuousOn, uniformEquicontinuous_restrict_iff, uniformEquicontinuousOn_iInf_rng, uniformEquicontinuousOn_unique, Filter.HasBasis.uniformEquicontinuousOn_iff_right, IsUniformInducing.uniformEquicontinuousOn_iff, Filter.HasBasis.uniformEquicontinuousOn_iff, UniformEquicontinuous.uniformEquicontinuousOn, uniformEquicontinuousOn_iff_uniformContinuousOn, uniformEquicontinuousOn_iff_range, uniformEquicontinuousOn_empty, uniformEquicontinuousOn_finite, Filter.HasBasis.uniformEquicontinuousOn_iff_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equicontinuousAt_empty 📖	mathematical	—	EquicontinuousAt	—	Filter.Eventually.of_forall
equicontinuousAt_finite 📖	mathematical	—	EquicontinuousAt ContinuousAt UniformSpace.toTopologicalSpace	—	forall_swap Filter.HasBasis.tendsto_right_iff nhds_basis_uniformity' Filter.basis_sets
equicontinuousAt_iInf_dom 📖	mathematical	EquicontinuousAt	iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	equicontinuousWithinAt_univ equicontinuousWithinAt_iInf_dom
equicontinuousAt_iInf_rng 📖	mathematical	—	EquicontinuousAt iInf UniformSpace instInfSetUniformSpace	—	equicontinuousWithinAt_univ
equicontinuousAt_iff_continuousAt 📖	mathematical	—	EquicontinuousAt ContinuousAt UniformFun UniformFun.topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.ofFun Function.swap	—	ContinuousAt.eq_1 Filter.HasBasis.tendsto_right_iff UniformFun.hasBasis_nhds
equicontinuousAt_iff_pair 📖	mathematical	—	EquicontinuousAt Set Filter Filter.instMembership nhds Set.instMembership	—	equicontinuousWithinAt_iff_pair Set.mem_univ nhdsWithin_univ
equicontinuousAt_iff_range 📖	mathematical	—	EquicontinuousAt Set Set.instMembership Set.range	—	Set.mem_range_self
equicontinuousAt_restrict_iff 📖	mathematical	—	EquicontinuousAt Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.restrict EquicontinuousWithinAt	—	—
equicontinuousAt_unique 📖	mathematical	—	EquicontinuousAt ContinuousAt UniformSpace.toTopologicalSpace Unique.instInhabited	—	equicontinuousAt_finite Finite.of_fintype Unique.forall_iff
equicontinuousOn_empty 📖	mathematical	—	EquicontinuousOn	—	equicontinuousWithinAt_empty
equicontinuousOn_finite 📖	mathematical	—	EquicontinuousOn ContinuousOn UniformSpace.toTopologicalSpace	—	forall_swap
equicontinuousOn_iInf_dom 📖	mathematical	EquicontinuousOn	iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	equicontinuousWithinAt_iInf_dom
equicontinuousOn_iInf_rng 📖	mathematical	—	EquicontinuousOn iInf UniformSpace instInfSetUniformSpace	—	forall_swap
equicontinuousOn_iff_continuousOn 📖	mathematical	—	EquicontinuousOn ContinuousOn UniformFun UniformFun.topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.ofFun Function.swap	—	—
equicontinuousOn_iff_range 📖	mathematical	—	EquicontinuousOn Set Set.instMembership Set.range	—	equicontinuousWithinAt_iff_range
equicontinuousOn_unique 📖	mathematical	—	EquicontinuousOn ContinuousOn UniformSpace.toTopologicalSpace Unique.instInhabited	—	equicontinuousOn_finite Finite.of_fintype Unique.forall_iff
equicontinuousOn_univ 📖	mathematical	—	EquicontinuousOn Set.univ Equicontinuous	—	—
equicontinuousWithinAt_empty 📖	mathematical	—	EquicontinuousWithinAt	—	Filter.Eventually.of_forall
equicontinuousWithinAt_finite 📖	mathematical	—	EquicontinuousWithinAt ContinuousWithinAt UniformSpace.toTopologicalSpace	—	forall_swap Filter.HasBasis.tendsto_right_iff nhds_basis_uniformity' Filter.basis_sets
equicontinuousWithinAt_iInf_dom 📖	mathematical	EquicontinuousWithinAt	iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	equicontinuousWithinAt_iff_continuousWithinAt nhds_iInf Filter.Tendsto.mono_left inf_le_inf_right iInf_le
equicontinuousWithinAt_iInf_rng 📖	mathematical	—	EquicontinuousWithinAt iInf UniformSpace instInfSetUniformSpace	—	equicontinuousWithinAt_iff_continuousWithinAt UniformFun.iInf_eq UniformSpace.toTopologicalSpace_iInf nhds_iInf Filter.tendsto_iInf
equicontinuousWithinAt_iff_continuousWithinAt 📖	mathematical	—	EquicontinuousWithinAt ContinuousWithinAt UniformFun UniformFun.topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.ofFun Function.swap	—	ContinuousWithinAt.eq_1 Filter.HasBasis.tendsto_right_iff UniformFun.hasBasis_nhds
equicontinuousWithinAt_iff_pair 📖	mathematical	Set Set.instMembership	EquicontinuousWithinAt Filter Filter.instMembership nhdsWithin	—	comp_symm_mem_uniformity_sets SetRel.prodMk_mem_comp SetRel.symm Filter.mp_mem Filter.univ_mem' mem_of_mem_nhdsWithin
equicontinuousWithinAt_iff_range 📖	mathematical	—	EquicontinuousWithinAt Set Set.instMembership Set.range	—	Set.mem_range_self
equicontinuousWithinAt_unique 📖	mathematical	—	EquicontinuousWithinAt ContinuousWithinAt UniformSpace.toTopologicalSpace Unique.instInhabited	—	equicontinuousWithinAt_finite Finite.of_fintype Unique.forall_iff
equicontinuousWithinAt_univ 📖	mathematical	—	EquicontinuousWithinAt Set.univ EquicontinuousAt	—	EquicontinuousWithinAt.eq_1 EquicontinuousAt.eq_1 nhdsWithin_univ
equicontinuous_empty 📖	mathematical	—	Equicontinuous	—	equicontinuousAt_empty
equicontinuous_finite 📖	mathematical	—	Equicontinuous Continuous UniformSpace.toTopologicalSpace	—	forall_swap
equicontinuous_iInf_dom 📖	mathematical	Equicontinuous	iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	equicontinuousAt_iInf_dom
equicontinuous_iInf_rng 📖	mathematical	—	Equicontinuous iInf UniformSpace instInfSetUniformSpace	—	equicontinuous_iff_continuous UniformFun.iInf_eq UniformSpace.toTopologicalSpace_iInf continuous_iInf_rng
equicontinuous_iff_continuous 📖	mathematical	—	Equicontinuous Continuous UniformFun UniformFun.topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.ofFun Function.swap	—	—
equicontinuous_iff_range 📖	mathematical	—	Equicontinuous Set Set.instMembership Set.range	—	equicontinuousAt_iff_range
equicontinuous_restrict_iff 📖	mathematical	—	Equicontinuous Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.restrict EquicontinuousOn	—	—
equicontinuous_unique 📖	mathematical	—	Equicontinuous Continuous UniformSpace.toTopologicalSpace Unique.instInhabited	—	equicontinuous_finite Finite.of_fintype Unique.forall_iff
uniformEquicontinuousOn_empty 📖	mathematical	—	UniformEquicontinuousOn	—	Filter.Eventually.of_forall
uniformEquicontinuousOn_finite 📖	mathematical	—	UniformEquicontinuousOn UniformContinuousOn	—	forall_swap
uniformEquicontinuousOn_iInf_dom 📖	mathematical	UniformEquicontinuousOn	iInf UniformSpace instInfSetUniformSpace	—	uniformEquicontinuousOn_iff_uniformContinuousOn iInf_uniformity Filter.Tendsto.mono_left inf_le_inf_right iInf_le
uniformEquicontinuousOn_iInf_rng 📖	mathematical	—	UniformEquicontinuousOn iInf UniformSpace instInfSetUniformSpace	—	uniformEquicontinuousOn_iff_uniformContinuousOn UniformFun.iInf_eq iInf_uniformity Filter.tendsto_iInf
uniformEquicontinuousOn_iff_range 📖	mathematical	—	UniformEquicontinuousOn Set Set.instMembership Set.range	—	Set.comp_rangeSplitting UniformEquicontinuousOn.comp
uniformEquicontinuousOn_iff_uniformContinuousOn 📖	mathematical	—	UniformEquicontinuousOn UniformContinuousOn UniformFun UniformFun.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.ofFun Function.swap	—	UniformContinuousOn.eq_1 Filter.HasBasis.tendsto_right_iff UniformFun.hasBasis_uniformity
uniformEquicontinuousOn_unique 📖	mathematical	—	UniformEquicontinuousOn UniformContinuousOn Unique.instInhabited	—	uniformEquicontinuousOn_finite Finite.of_fintype Unique.forall_iff
uniformEquicontinuousOn_univ 📖	mathematical	—	UniformEquicontinuousOn Set.univ UniformEquicontinuous	—	Set.univ_prod_univ Filter.principal_univ inf_of_le_left
uniformEquicontinuous_empty 📖	mathematical	—	UniformEquicontinuous	—	Filter.Eventually.of_forall
uniformEquicontinuous_finite 📖	mathematical	—	UniformEquicontinuous UniformContinuous	—	forall_swap
uniformEquicontinuous_iInf_dom 📖	mathematical	UniformEquicontinuous	iInf UniformSpace instInfSetUniformSpace	—	uniformEquicontinuous_iff_uniformContinuous uniformContinuous_iInf_dom
uniformEquicontinuous_iInf_rng 📖	mathematical	—	UniformEquicontinuous iInf UniformSpace instInfSetUniformSpace	—	uniformEquicontinuous_iff_uniformContinuous UniformFun.iInf_eq uniformContinuous_iInf_rng
uniformEquicontinuous_iff_range 📖	mathematical	—	UniformEquicontinuous Set Set.instMembership Set.range	—	Set.comp_rangeSplitting UniformEquicontinuous.comp
uniformEquicontinuous_iff_uniformContinuous 📖	mathematical	—	UniformEquicontinuous UniformContinuous UniformFun UniformFun.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.ofFun Function.swap	—	UniformContinuous.eq_1 Filter.HasBasis.tendsto_right_iff UniformFun.hasBasis_uniformity
uniformEquicontinuous_restrict_iff 📖	mathematical	—	UniformEquicontinuous Set.Elem instUniformSpaceSubtype Set Set.instMembership Set.restrict UniformEquicontinuousOn	—	UniformEquicontinuous.eq_1 UniformEquicontinuousOn.eq_1 Subtype.range_val Set.range_prodMap Filter.map_comap
uniformEquicontinuous_unique 📖	mathematical	—	UniformEquicontinuous UniformContinuous Unique.instInhabited	—	uniformEquicontinuous_finite Finite.of_fintype Unique.forall_iff

---

← Back to Index