CompactConvergence

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

Statistics

Metric	Count
Definitions `compactConvergenceUniformSpace`, `toUniformOnFunIsCompact`, `arrowCongr`	3
Theorems `hasAntitoneBasis_compactConvergenceUniformity`, `hasBasis_compactConvergenceUniformity`, `continuous_iff_continuous_uniformFun`, `continuous_iff_continuous_uniformOnFun`, `hasBasis_compactConvergenceUniformity`, `hasBasis_compactConvergenceUniformity_of_compact`, `instCompleteSpaceOfCompactlyCoherentSpace`, `instIsCountablyGeneratedProdUniformityOfWeaklyLocallyCompactSpaceOfSigmaCompactSpace`, `isComplete_setOf_eqOn`, `isUniformEmbedding_comp`, `isUniformEmbedding_toUniformOnFunIsCompact`, `isUniformEmbedding_uniformFunOfFun`, `isUniformInducing_comp`, `mem_compactConvergence_entourage_iff`, `range_toUniformOnFunIsCompact`, `tendsto_iff_forall_isCompact_tendstoUniformlyOn`, `tendsto_iff_tendstoLocallyUniformly`, `tendsto_iff_tendstoUniformly`, `tendsto_of_tendstoLocallyUniformly`, `toUniformOnFun_toFun`, `uniformContinuous_comp`, `uniformContinuous_comp_left`, `uniformSpace_eq_iInf_precomp_of_cover`, `uniformSpace_eq_inf_precomp_of_cover`, `continuous_restrict_iff_continuous_uniformOnFun`, `tendsto_restrict_iff_tendstoUniformlyOn`, `compactConvergenceUniformity`, `compactConvergenceUniformity_of_compact`	28
Total	31

CompactExhaustion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasAntitoneBasis_compactConvergenceUniformity` 📖	mathematical	`Filter.HasAntitoneBasis` `Nat.instPreorder` `uniformity`	`ContinuousMap` `UniformSpace.toTopologicalSpace` `ContinuousMap.compactConvergenceUniformSpace` `setOf`	—	`Filter.HasAntitoneBasis.comap` `UniformOnFun.hasAntitoneBasis_uniformity` `SemilatticeSup.instIsDirectedOrder` `isCompact` `subset` `exists_superset_of_isCompact`
`hasBasis_compactConvergenceUniformity` 📖	mathematical	`Filter.HasBasis` `uniformity`	`ContinuousMap` `UniformSpace.toTopologicalSpace` `ContinuousMap.compactConvergenceUniformSpace` `setOf`	—	`Filter.HasBasis.comap` `UniformOnFun.hasBasis_uniformity_of_covering_of_basis` `isCompact` `Monotone.directed_le` `SemilatticeSup.instIsDirectedOrder` `subset` `exists_superset_of_isCompact`

ContinuousMap

Definitions

Name	Category	Theorems
`compactConvergenceUniformSpace` 📖	CompOp	24 math math: `isUniformInducing_equivBoundedOfCompact`, `ODE.FunSpace.isUniformInducing_toContinuousMap`, `mem_compactConvergence_entourage_iff`, `uniformContinuous_comp_left`, `Path.uniformContinuous_extend_left`, `hasBasis_compactConvergenceUniformity`, `uniformContinuous_comp`, `Path.isUniformEmbedding_coe`, `instCompleteSpaceOfCompactlyCoherentSpace`, `CompactExhaustion.hasAntitoneBasis_compactConvergenceUniformity`, `isUniformEmbedding_comp`, `isUniformEmbedding_toUniformOnFunIsCompact`, `isUniformEmbedding_uniformFunOfFun`, `ContinuousMapZero.isUniformEmbedding_toContinuousMap`, `Filter.HasBasis.compactConvergenceUniformity_of_compact`, `hasBasis_compactConvergenceUniformity_of_compact`, `isUniformInducing_comp`, `isComplete_setOf_eqOn`, `instIsCountablyGeneratedProdUniformityOfWeaklyLocallyCompactSpaceOfSigmaCompactSpace`, `Filter.HasBasis.compactConvergenceUniformity`, `uniformSpace_eq_iInf_precomp_of_cover`, `CompactExhaustion.hasBasis_compactConvergenceUniformity`, `isUniformEmbedding_equivBoundedOfCompact`, `uniformSpace_eq_inf_precomp_of_cover`
`toUniformOnFunIsCompact` 📖	CompOp	3 math math: `toUniformOnFun_toFun`, `isUniformEmbedding_toUniformOnFunIsCompact`, `range_toUniformOnFunIsCompact`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_iff_continuous_uniformFun` 📖	mathematical	—	`Continuous` `ContinuousMap` `UniformSpace.toTopologicalSpace` `compactOpen` `UniformFun` `UniformFun.topologicalSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `UniformFun.ofFun` `instFunLike`	—	`Topology.IsInducing.continuous_iff` `IsUniformInducing.isInducing` `IsUniformEmbedding.toIsUniformInducing` `isUniformEmbedding_uniformFunOfFun`
`continuous_iff_continuous_uniformOnFun` 📖	mathematical	—	`Continuous` `ContinuousMap` `UniformSpace.toTopologicalSpace` `compactOpen` `UniformOnFun` `setOf` `Set` `IsCompact` `UniformOnFun.topologicalSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `UniformOnFun.ofFun` `instFunLike`	—	`Topology.IsInducing.continuous_iff` `IsUniformInducing.isInducing` `IsUniformEmbedding.toIsUniformInducing` `isUniformEmbedding_toUniformOnFunIsCompact`
`hasBasis_compactConvergenceUniformity` 📖	mathematical	—	`Filter.HasBasis` `ContinuousMap` `UniformSpace.toTopologicalSpace` `Set` `uniformity` `compactConvergenceUniformSpace` `IsCompact` `Filter` `Filter.instMembership` `setOf`	—	`Filter.HasBasis.compactConvergenceUniformity` `Filter.basis_sets`
`hasBasis_compactConvergenceUniformity_of_compact` 📖	mathematical	—	`Filter.HasBasis` `ContinuousMap` `UniformSpace.toTopologicalSpace` `Set` `uniformity` `compactConvergenceUniformSpace` `Filter` `Filter.instMembership` `setOf`	—	`Filter.HasBasis.to_hasBasis` `hasBasis_compactConvergenceUniformity` `isCompact_univ` `Set.mem_univ`
`instCompleteSpaceOfCompactlyCoherentSpace` 📖	mathematical	—	`CompleteSpace` `ContinuousMap` `UniformSpace.toTopologicalSpace` `compactConvergenceUniformSpace`	—	`completeSpace_iff_isComplete_range` `IsUniformEmbedding.isUniformInducing` `isUniformEmbedding_toUniformOnFunIsCompact` `range_toUniformOnFunIsCompact` `completeSpace_coe_iff_isComplete` `IsClosed.completeSpace_coe` `UniformOnFun.instCompleteSpace` `UniformOnFun.isClosed_setOf_continuous` `CompactlyCoherentSpace.isCoherentWith`
`instIsCountablyGeneratedProdUniformityOfWeaklyLocallyCompactSpaceOfSigmaCompactSpace` 📖	mathematical	—	`Filter.IsCountablyGenerated` `ContinuousMap` `UniformSpace.toTopologicalSpace` `uniformity` `compactConvergenceUniformSpace`	—	`Filter.exists_antitone_basis` `Filter.HasBasis.isCountablyGenerated` `instCountableNat` `Filter.HasAntitoneBasis.toHasBasis` `CompactExhaustion.hasAntitoneBasis_compactConvergenceUniformity`
`isComplete_setOf_eqOn` 📖	mathematical	—	`IsComplete` `ContinuousMap` `UniformSpace.toTopologicalSpace` `compactConvergenceUniformSpace` `setOf` `Set.EqOn` `DFunLike.coe` `instFunLike`	—	`CompleteSpace.complete` `tendsto_nhds_unique_inseparable` `instR1Space` `UniformSpace.to_regularSpace` `Filter.Tendsto.congr'` `Filter.EventuallyEq.filter_mono` `tendsto_const_nhds` `Filter.Tendsto.mono_left` `Continuous.continuousAt` `ContinuousEvalConst.continuous_eval_const` `instContinuousEvalConst` `Set.piecewise_eq_of_mem` `Set.piecewise_eq_of_notMem` `continuous_congr_of_inseparable` `ContinuousMapClass.map_continuous` `instContinuousMapClass` `Set.piecewise_eqOn` `LE.le.trans_eq` `Inseparable.eq_1` `inseparable_coe` `inseparable_pi`
`isUniformEmbedding_comp` 📖	mathematical	`IsUniformEmbedding` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `instFunLike`	`compactConvergenceUniformSpace` `comp`	—	`IsUniformEmbedding.of_comp_iff` `isUniformEmbedding_toUniformOnFunIsCompact` `IsUniformEmbedding.comp` `UniformOnFun.postcomp_isUniformEmbedding`
`isUniformEmbedding_toUniformOnFunIsCompact` 📖	mathematical	—	`IsUniformEmbedding` `ContinuousMap` `UniformSpace.toTopologicalSpace` `UniformOnFun` `setOf` `Set` `IsCompact` `compactConvergenceUniformSpace` `UniformOnFun.uniformSpace` `toUniformOnFunIsCompact`	—	`DFunLike.coe_injective`
`isUniformEmbedding_uniformFunOfFun` 📖	mathematical	—	`IsUniformEmbedding` `ContinuousMap` `UniformSpace.toTopologicalSpace` `UniformFun` `compactConvergenceUniformSpace` `UniformFun.uniformSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `UniformFun.ofFun` `instFunLike`	—	`IsUniformEmbedding.toIsUniformInducing` `isCompact_univ` `IsUniformEmbedding.comp` `UniformEquiv.isUniformEmbedding` `isUniformEmbedding_toUniformOnFunIsCompact` `DFunLike.coe_injective`
`isUniformInducing_comp` 📖	mathematical	`IsUniformInducing` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `instFunLike`	`compactConvergenceUniformSpace` `comp`	—	`IsUniformInducing.of_comp_iff` `IsUniformEmbedding.isUniformInducing` `isUniformEmbedding_toUniformOnFunIsCompact` `IsUniformInducing.comp` `UniformOnFun.postcomp_isUniformInducing`
`mem_compactConvergence_entourage_iff` 📖	mathematical	—	`Set` `ContinuousMap` `UniformSpace.toTopologicalSpace` `Filter` `Filter.instMembership` `uniformity` `compactConvergenceUniformSpace` `IsCompact` `Set.instHasSubset` `setOf`	—	`Filter.HasBasis.mem_iff` `hasBasis_compactConvergenceUniformity`
`range_toUniformOnFunIsCompact` 📖	mathematical	—	`Set.range` `UniformOnFun` `setOf` `Set` `IsCompact` `ContinuousMap` `UniformSpace.toTopologicalSpace` `toUniformOnFunIsCompact` `Continuous`	—	`Set.ext` `continuous_toFun`
`tendsto_iff_forall_isCompact_tendstoUniformlyOn` 📖	mathematical	—	`Filter.Tendsto` `ContinuousMap` `UniformSpace.toTopologicalSpace` `nhds` `compactOpen` `TendstoUniformlyOn` `DFunLike.coe` `instFunLike`	—	`tendsto_nhds_compactOpen` `tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact` `comp_open_symm_mem_uniformity_sets` `mem_uniformity_isClosed` `inter_mem_nhdsWithin` `continuousAt` `UniformSpace.ball_mem_nhds` `IsCompact.inter_right` `IsClosed.preimage` `continuous` `UniformSpace.isClosed_ball` `Filter.Eventually.mono` `UniformSpace.isOpen_ball` `SetRel.symm` `lebesgue_number_of_compact_open` `IsCompact.image` `ContinuousMapClass.map_continuous` `instContinuousMapClass` `Set.MapsTo.image_subset` `Filter.mp_mem` `Filter.univ_mem'` `Set.mem_image_of_mem`
`tendsto_iff_tendstoLocallyUniformly` 📖	mathematical	—	`Filter.Tendsto` `ContinuousMap` `UniformSpace.toTopologicalSpace` `nhds` `compactOpen` `TendstoLocallyUniformly` `DFunLike.coe` `instFunLike`	—	`WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `tendsto_iff_forall_isCompact_tendstoUniformlyOn` `tendsto_of_tendstoLocallyUniformly`
`tendsto_iff_tendstoUniformly` 📖	mathematical	—	`Filter.Tendsto` `ContinuousMap` `UniformSpace.toTopologicalSpace` `nhds` `compactOpen` `TendstoUniformly` `DFunLike.coe` `instFunLike`	—	`Topology.IsInducing.tendsto_nhds_iff` `IsUniformInducing.isInducing` `IsUniformEmbedding.toIsUniformInducing` `isUniformEmbedding_uniformFunOfFun`
`tendsto_of_tendstoLocallyUniformly` 📖	mathematical	`TendstoLocallyUniformly` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `instFunLike`	`Filter.Tendsto` `nhds` `compactOpen`	—	`tendsto_iff_forall_isCompact_tendstoUniformlyOn` `tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact` `TendstoLocallyUniformly.tendstoLocallyUniformlyOn`
`toUniformOnFun_toFun` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `setOf` `Set` `IsCompact` `EquivLike.toFunLike` `Equiv.instEquivLike` `UniformOnFun.toFun` `toUniformOnFunIsCompact` `ContinuousMap` `UniformSpace.toTopologicalSpace` `instFunLike`	—	—
`uniformContinuous_comp` 📖	mathematical	`UniformContinuous` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `instFunLike`	`compactConvergenceUniformSpace` `comp`	—	`IsUniformInducing.uniformContinuous_iff` `IsUniformEmbedding.toIsUniformInducing` `isUniformEmbedding_toUniformOnFunIsCompact` `UniformContinuous.comp` `UniformOnFun.postcomp_uniformContinuous` `IsUniformInducing.uniformContinuous`
`uniformContinuous_comp_left` 📖	mathematical	—	`UniformContinuous` `ContinuousMap` `UniformSpace.toTopologicalSpace` `compactConvergenceUniformSpace` `comp`	—	`IsUniformInducing.uniformContinuous_iff` `IsUniformEmbedding.toIsUniformInducing` `isUniformEmbedding_toUniformOnFunIsCompact` `UniformContinuous.comp` `UniformOnFun.precomp_uniformContinuous` `IsCompact.image` `continuous` `IsUniformInducing.uniformContinuous`
`uniformSpace_eq_iInf_precomp_of_cover` 📖	mathematical	`IsProperMap` `DFunLike.coe` `ContinuousMap` `instFunLike` `LocallyFinite` `Set.range` `Set.iUnion` `Set.univ`	`UniformSpace` `UniformSpace.toTopologicalSpace` `compactConvergenceUniformSpace` `iInf` `instInfSetUniformSpace` `UniformSpace.comap` `comp`	—	`IsCompact.image` `continuous` `IsProperMap.isCompact_preimage` `LocallyFinite.finite_nonempty_inter_compact` `Set.inter_eq_right` `Set.iUnion₂_inter` `Set.iUnion_congr_Prop` `Set.iUnion_nonempty_self` `Set.univ_inter` `UniformSpace.replaceTopology_eq` `UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover` `UniformSpace.comap_iInf`
`uniformSpace_eq_inf_precomp_of_cover` 📖	mathematical	`IsProperMap` `DFunLike.coe` `ContinuousMap` `instFunLike` `Set` `Set.instUnion` `Set.range` `Set.univ`	`UniformSpace` `UniformSpace.toTopologicalSpace` `compactConvergenceUniformSpace` `instMinUniformSpace` `UniformSpace.comap` `comp`	—	`IsCompact.image` `continuous` `IsProperMap.isCompact_preimage` `Set.subset_univ` `UniformSpace.replaceTopology_eq` `UniformOnFun.uniformSpace_eq_inf_precomp_of_cover` `UniformSpace.comap_inf`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_restrict_iff_continuous_uniformOnFun` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace`	`Continuous` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `ContinuousMap.compactOpen` `Set.restrict` `restrict` `UniformOnFun` `Set.instSingletonSet` `UniformOnFun.topologicalSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `UniformOnFun.ofFun`	—	`restrict` `ContinuousMap.continuous_iff_continuous_uniformFun` `UniformOnFun.continuous_rng_iff`
`tendsto_restrict_iff_tendstoUniformlyOn` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace`	`Filter.Tendsto` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `restrict` `nhds` `ContinuousMap.compactOpen` `TendstoUniformlyOn`	—	`restrict` `ContinuousMap.tendsto_iff_tendstoUniformly` `tendstoUniformlyOn_iff_tendstoUniformly_comp_coe`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactConvergenceUniformity` 📖	mathematical	`Filter.HasBasis` `uniformity`	`ContinuousMap` `UniformSpace.toTopologicalSpace` `Set` `ContinuousMap.compactConvergenceUniformSpace` `IsCompact` `setOf`	—	`IsUniformInducing.comap_uniformity` `IsUniformEmbedding.toIsUniformInducing` `ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact` `comap` `UniformOnFun.hasBasis_uniformity_of_basis` `isCompact_empty` `directedOn_of_sup_mem` `IsCompact.union`
`compactConvergenceUniformity_of_compact` 📖	mathematical	`Filter.HasBasis` `uniformity`	`ContinuousMap` `UniformSpace.toTopologicalSpace` `ContinuousMap.compactConvergenceUniformSpace` `setOf`	—	`to_hasBasis` `ContinuousMap.hasBasis_compactConvergenceUniformity_of_compact` `mem_iff` `mem_of_mem` `Set.Subset.rfl`

UniformEquiv

Definitions

Name	Category	Theorems
`arrowCongr` 📖	CompOp	—

---

← Back to Index