HeineCantor

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

Statistics

Metric	Count
Definitions	0
Theorems uniformContinuous_of_continuous, uniformEquicontinuous_of_equicontinuous, tendstoUniformly, uniformContinuous_of_tendsto_cocompact, tendstoUniformly, uniformContinuous_of_continuous, uniformContinuous_of_continuous, mem_uniformity_of_prod, uniformContinuousAt_of_continuousAt, uniformContinuousOn_of_continuous	10
Total	10

CompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformContinuous_of_continuous 📖	mathematical	Continuous UniformSpace.toTopologicalSpace	UniformContinuous	—	nhdsSet_diagonal_eq_uniformity Continuous.tendsto_nhdsSet Continuous.prodMap Set.mapsTo_prodMap_diagonal nhdsSet_diagonal_le_uniformity
uniformEquicontinuous_of_equicontinuous 📖	mathematical	Equicontinuous UniformSpace.toTopologicalSpace	UniformEquicontinuous	—	uniformEquicontinuous_iff_uniformContinuous uniformContinuous_of_continuous equicontinuous_iff_continuous

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendstoUniformly 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase	TendstoUniformly nhds	—	WeaklyLocallyCompactSpace.exists_compact_mem_nhds IsCompact.uniformContinuousOn_of_continuous IsCompact.prod isCompact_univ continuousOn UniformContinuousOn.tendstoUniformly
uniformContinuous_of_tendsto_cocompact 📖	mathematical	Continuous UniformSpace.toTopologicalSpace Filter.Tendsto Filter.cocompact nhds	UniformContinuous	—	uniformContinuous_def comp_symm_mem_uniformity_sets Filter.mem_cocompact mem_nhds_left Filter.mem_of_superset symmetrize_mem_uniformity IsCompact.uniformContinuousAt_of_continuousAt continuousAt SetRel.symm

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendstoUniformly 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace ContinuousOn instTopologicalSpaceProd Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase SProd.sprod Set.instSProd Set.univ	TendstoUniformly	—	LocallyCompactSpace.local_compact_nhds IsCompact.uniformContinuousOn_of_continuous IsCompact.prod isCompact_univ mono Set.prod_mono Set.Subset.rfl UniformContinuousOn.tendstoUniformly

HasCompactMulSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformContinuous_of_continuous 📖	mathematical	HasCompactMulSupport UniformSpace.toTopologicalSpace Continuous	UniformContinuous	—	Continuous.uniformContinuous_of_tendsto_cocompact is_one_at_infty

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformContinuous_of_continuous 📖	mathematical	HasCompactSupport UniformSpace.toTopologicalSpace Continuous	UniformContinuous	—	Continuous.uniformContinuous_of_tendsto_cocompact is_zero_at_infty

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_uniformity_of_prod 📖	mathematical	IsCompact ContinuousOn instTopologicalSpaceProd UniformSpace.toTopologicalSpace SProd.sprod Set Set.instSProd Set.instMembership Filter Filter.instMembership uniformity	nhdsWithin	—	induction_on Filter.univ_mem instIsEmptyFalse Filter.inter_mem comp_symm_of_uniformity mem_nhdsWithin_prod_iff mem_nhds_left mem_of_mem_nhdsWithin SetRel.prodMk_mem_comp
uniformContinuousAt_of_continuousAt 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace ContinuousAt Set Filter Filter.instMembership uniformity	setOf	—	comp_symm_mem_uniformity_sets elim_nhds_subcover' Filter.mem_of_superset Filter.biInter_finset_mem Set.mem_iUnion₂ SetRel.symm UniformSpace.mem_ball_self Set.mem_iInter₂ exists_mem_nhds_ball_subset_of_mem_nhds ContinuousAt.preimage_mem_nhds mem_nhds_left
uniformContinuousOn_of_continuous 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace ContinuousOn	UniformContinuousOn	—	uniformContinuousOn_iff_restrict CompactSpace.uniformContinuous_of_continuous isCompact_iff_compactSpace continuousOn_iff_continuous_restrict

---

← Back to Index