Ascoli

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

Statistics

Metric	Count
Definitions	0
Theorems compactSpace_of_closed_inducing', compactSpace_of_isClosedEmbedding, isCompact_closure_of_isClosedEmbedding, isCompact_of_equicontinuous, comap_uniformFun_eq, inducing_uniformFun_iff_pi, isUniformInducing_uniformFun_iff_pi, tendsto_uniformFun_iff_pi, comap_uniformOnFun_eq, inducing_uniformOnFun_iff_pi', isClosed_range_pi_of_uniformOnFun, isClosed_range_pi_of_uniformOnFun', isClosed_range_uniformOnFun_iff_pi, isInducing_uniformOnFun_iff_pi, isUniformInducing_uniformOnFun_iff_pi, isUniformInducing_uniformOnFun_iff_pi', tendsto_uniformOnFun_iff_pi, tendsto_uniformOnFun_iff_pi'	18
Total	18

ArzelaAscoli

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace_of_closed_inducing' 📖	mathematical	IsCompact Topology.IsInducing UniformOnFun UniformOnFun.topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun EquicontinuousOn UniformSpace.toTopologicalSpace Set Set.instMembership	CompactSpace	—	EquicontinuousOn.inducing_uniformOnFun_iff_pi' isCompact_univ_iff Topology.IsInducing.isCompact_iff Set.image_univ IsCompact.of_isClosed_subset isCompact_univ_pi EquicontinuousOn.isClosed_range_pi_of_uniformOnFun' Set.range_subset_iff forall_sUnion Function.sometimes_spec
compactSpace_of_isClosedEmbedding 📖	mathematical	IsCompact Topology.IsClosedEmbedding UniformOnFun UniformOnFun.topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun EquicontinuousOn UniformSpace.toTopologicalSpace Set Set.instMembership	CompactSpace	—	compactSpace_of_closed_inducing' Topology.IsClosedEmbedding.isInducing Topology.IsClosedEmbedding.isClosed_range
isCompact_closure_of_isClosedEmbedding 📖	mathematical	IsCompact Topology.IsClosedEmbedding UniformOnFun UniformOnFun.topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun EquicontinuousOn Set Set.instMembership UniformSpace.toTopologicalSpace	closure	—	isCompact_iff_compactSpace Continuous.comp UniformContinuous.continuous UniformOnFun.uniformContinuous_eval_of_mem Topology.IsClosedEmbedding.continuous EquicontinuousOn.closure' continuous_pi closure_minimal IsClosed.preimage IsCompact.isClosed compactSpace_of_isClosedEmbedding Topology.IsClosedEmbedding.comp IsClosed.isClosedEmbedding_subtypeVal isClosed_closure
isCompact_of_equicontinuous 📖	mathematical	IsCompact Pi.topologicalSpace UniformSpace.toTopologicalSpace Set.image ContinuousMap ContinuousMap.toFun Equicontinuous Set.Elem DFunLike.coe ContinuousMap.instFunLike Set Set.instMembership	ContinuousMap.compactOpen	—	DFunLike.coe_injective Topology.IsInducing.of_comp_iff Topology.IsInducing.subtypeVal EquicontinuousOn.isInducing_uniformOnFun_iff_pi Set.eq_univ_iff_forall Set.mem_sUnion_of_mem Set.mem_singleton isCompact_singleton Equicontinuous.equicontinuousOn Topology.IsInducing.comp IsUniformInducing.isInducing IsUniformEmbedding.toIsUniformInducing ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact isCompact_iff_compactSpace Homeomorph.compactSpace

Equicontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_uniformFun_eq 📖	mathematical	Equicontinuous	UniformSpace.comap UniformFun.uniformSpace Pi.uniformSpace	—	le_antisymm UniformSpace.comap_mono UniformFun.uniformContinuous_toFun Pi.uniformity Filter.comap_iInf Filter.comap_comap Filter.HasBasis.ge_iff Filter.HasBasis.comap UniformFun.hasBasis_uniformity comp_comp_symm_mem_uniformity_sets CompactSpace.elim_nhds_subcover Set.mem_iUnion₂ Eq.subset Set.instReflSubset Set.mem_univ SetRel.prodMk_mem_comp SetRel.symm Set.mem_iInter₂ Filter.mem_of_superset Finset.iInter_mem_sets Filter.mem_iInf_of_mem Filter.preimage_mem_comap
inducing_uniformFun_iff_pi 📖	mathematical	Equicontinuous	Topology.IsInducing UniformFun UniformFun.topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.ofFun Pi.topologicalSpace UniformSpace.toTopologicalSpace	—	Topology.isInducing_iff comap_uniformFun_eq
isUniformInducing_uniformFun_iff_pi 📖	mathematical	Equicontinuous	IsUniformInducing UniformFun UniformFun.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.ofFun Pi.uniformSpace	—	isUniformInducing_iff_uniformSpace comap_uniformFun_eq
tendsto_uniformFun_iff_pi 📖	mathematical	Equicontinuous	Filter.Tendsto UniformFun DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformFun.ofFun nhds UniformFun.topologicalSpace Pi.topologicalSpace UniformSpace.toTopologicalSpace	—	Filter.eq_or_neBot Filter.Tendsto.comp Continuous.tendsto UniformContinuous.continuous UniformFun.uniformContinuous_toFun closure' equicontinuous_iff_range continuous_id inducing_uniformFun_iff_pi mem_closure_of_tendsto Filter.range_mem_map Filter.map_comap_of_mem Filter.mem_of_superset subset_closure Subtype.range_coe Filter.tendsto_id' nhds_induced Filter.map_le_iff_le_comap Filter.tendsto_map'_iff Topology.IsInducing.tendsto_nhds_iff

EquicontinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_uniformOnFun_eq 📖	mathematical	IsCompact EquicontinuousOn	UniformSpace.comap UniformOnFun.uniformSpace Set.restrict Set.sUnion Pi.uniformSpace Set.Elem	—	UniformSpace.comap_iInf iInf_congr_Prop UniformSpace.comap_comap Pi.uniformSpace_comap_restrict_sUnion isCompact_iff_compactSpace Equicontinuous.comap_uniformFun_eq equicontinuous_restrict_iff iInf_congr
inducing_uniformOnFun_iff_pi' 📖	mathematical	IsCompact EquicontinuousOn	Topology.IsInducing UniformOnFun UniformOnFun.topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun Pi.topologicalSpace Set.Elem Set.sUnion UniformSpace.toTopologicalSpace Set.restrict	—	Topology.isInducing_iff comap_uniformOnFun_eq
isClosed_range_pi_of_uniformOnFun 📖	mathematical	IsCompact Set.sUnion Set.univ EquicontinuousOn	IsClosed Pi.topologicalSpace UniformSpace.toTopologicalSpace Set.range	—	isClosed_range_uniformOnFun_iff_pi
isClosed_range_pi_of_uniformOnFun' 📖	mathematical	IsCompact EquicontinuousOn	IsClosed Pi.topologicalSpace Set.Elem Set.sUnion UniformSpace.toTopologicalSpace Set.range Set.restrict	—	isEmpty_or_nonempty Finite.instDiscreteTopology instT1SpaceForall T2Space.t1Space DiscreteTopology.toT2Space Subsingleton.discreteTopology IsEmpty.instSubsingleton Finite.of_subsingleton Set.range_comp Function.Surjective.forall Function.Injective.surjective_comp_right Subtype.coe_injective tendsto_uniformOnFun_iff_pi' Set.mem_image_of_mem IsClosed.mem_of_tendsto Ultrafilter.neBot Filter.Eventually.of_forall Set.mem_range_self
isClosed_range_uniformOnFun_iff_pi 📖	mathematical	IsCompact Set.sUnion Set.univ EquicontinuousOn	IsClosed UniformOnFun UniformOnFun.topologicalSpace Set.range DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun Pi.topologicalSpace UniformSpace.toTopologicalSpace	—	Set.range_comp Function.Surjective.forall Equiv.surjective tendsto_uniformOnFun_iff_pi Function.Injective.mem_set_image Equiv.injective
isInducing_uniformOnFun_iff_pi 📖	mathematical	Set.sUnion Set.univ IsCompact EquicontinuousOn	Topology.IsInducing UniformOnFun UniformOnFun.topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun Pi.topologicalSpace UniformSpace.toTopologicalSpace	—	Set.eq_univ_iff_forall inducing_uniformOnFun_iff_pi' Topology.IsInducing.comp Homeomorph.isInducing
isUniformInducing_uniformOnFun_iff_pi 📖	mathematical	Set.sUnion Set.univ IsCompact EquicontinuousOn	IsUniformInducing UniformOnFun UniformOnFun.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun Pi.uniformSpace	—	Set.eq_univ_iff_forall isUniformInducing_uniformOnFun_iff_pi' IsUniformInducing.comp UniformEquiv.isUniformInducing
isUniformInducing_uniformOnFun_iff_pi' 📖	mathematical	IsCompact EquicontinuousOn	IsUniformInducing UniformOnFun UniformOnFun.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun Pi.uniformSpace Set.Elem Set.sUnion Set.restrict	—	isUniformInducing_iff_uniformSpace comap_uniformOnFun_eq
tendsto_uniformOnFun_iff_pi 📖	mathematical	IsCompact Set.sUnion Set.univ EquicontinuousOn	Filter.Tendsto UniformOnFun DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun nhds UniformOnFun.topologicalSpace Pi.topologicalSpace UniformSpace.toTopologicalSpace	—	Set.eq_univ_iff_forall tendsto_uniformOnFun_iff_pi' Topology.IsInducing.tendsto_nhds_iff Homeomorph.isInducing
tendsto_uniformOnFun_iff_pi' 📖	mathematical	IsCompact EquicontinuousOn	Filter.Tendsto UniformOnFun DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun nhds UniformOnFun.topologicalSpace Set.restrict Set.sUnion Pi.topologicalSpace Set.Elem UniformSpace.toTopologicalSpace	—	Filter.tendsto_comap_iff nhds_induced UniformOnFun.topologicalSpace_eq Pi.induced_restrict_sUnion nhds_iInf iInf_congr_Prop isCompact_iff_compactSpace Equicontinuous.tendsto_uniformFun_iff_pi equicontinuous_restrict_iff

---

← Back to Index