UniformEmbedding

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

Statistics

Metric	Count
Definitions `comapUniformSpace`	1
Theorems `sum`, `extend_exists`, `extend_of_ind`, `extend_spec`, `uniformContinuous_extend`, `to_isUniformEmbedding`, `isUniformEmbedding`, `isUniformEmbedding_iff`, `isUniformEmbedding_iff'`, `isUniformInducing_iff`, `totallyBounded_comap`, `totallyBounded_map_iff`, `completeSpace_coe`, `completeSpace_coe`, `isUniformInducing_extend`, `comp`, `discreteUniformity`, `isComplete_iff`, `isDenseEmbedding`, `isEmbedding`, `of_comp_iff`, `prod`, `basis_uniformity`, `cauchy_map_iff`, `comap_uniformSpace`, `comp`, `completeSpace`, `completeSpace_congr`, `id`, `injective`, `isComplete_iff`, `isComplete_range`, `isDenseInducing`, `isInducing`, `isUniformEmbedding`, `isUniformInducing_comp_iff`, `mk'`, `of_comp`, `of_comp_iff`, `prod`, `rangeFactorization`, `uniformContinuous`, `uniformContinuousOn_iff`, `uniformContinuous_iff`, `completeSpace_iff`, `instCompleteSpace`, `isUniformInducing_mk`, `isComplete_iff`, `instCompleteSpace`, `rangeFactorization`, `closure_image_mem_nhds_of_isUniformInducing`, `comap_uniformity_of_spaced_out`, `completeSpace_coe_iff_isComplete`, `completeSpace_congr`, `completeSpace_extension`, `completeSpace_iff_isComplete_range`, `completeSpace_ulift_iff`, `isClosedEmbedding_of_spaced_out`, `isComplete_image_iff`, `isComplete_of_complete_image`, `isUniformEmbedding_comap`, `isUniformEmbedding_iff'`, `isUniformEmbedding_iff_isUniformInducing`, `isUniformEmbedding_inl`, `isUniformEmbedding_inr`, `isUniformEmbedding_of_spaced_out`, `isUniformEmbedding_set_inclusion`, `isUniformEmbedding_subtypeEmb`, `isUniformEmbedding_subtype_val`, `isUniformInducing_iff'`, `isUniformInducing_iff_uniformSpace`, `isUniformInducing_rangeFactorization_iff`, `isUniformInducing_val`, `totallyBounded_image_iff`, `totallyBounded_preimage`, `uniformContinuous_rangeFactorization_iff`, `uniformContinuous_uniformly_extend`, `uniform_extend_subtype`, `uniformly_extend_exists`, `uniformly_extend_of_ind`, `uniformly_extend_spec`, `uniformly_extend_unique`	82
Total	83

CompleteSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum` 📖	mathematical	—	`CompleteSpace` `Sum.instUniformSpace`	—	`completeSpace_iff_isComplete_univ` `Set.range_inl_union_range_inr` `IsComplete.union` `IsUniformInducing.isComplete_range` `IsUniformEmbedding.isUniformInducing` `isUniformEmbedding_inl` `isUniformEmbedding_inr`

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extend_exists` 📖	mathematical	`Dense` `UniformSpace.toTopologicalSpace` `UniformContinuous` `Set.Elem` `instUniformSpaceSubtype` `Set` `Set.instMembership`	`Filter.Tendsto` `Filter.comap` `nhds`	—	`uniformly_extend_exists` `isUniformInducing_val` `denseRange_val`
`extend_of_ind` 📖	mathematical	`Dense` `UniformSpace.toTopologicalSpace` `UniformContinuous` `Set.Elem` `instUniformSpaceSubtype` `Set` `Set.instMembership`	`extend`	—	`IsDenseInducing.extend_eq_at` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `UniformSpace.to_regularSpace` `isDenseInducing_val` `Continuous.continuousAt` `UniformContinuous.continuous`
`extend_spec` 📖	mathematical	`Dense` `UniformSpace.toTopologicalSpace` `UniformContinuous` `Set.Elem` `instUniformSpaceSubtype` `Set` `Set.instMembership`	`Filter.Tendsto` `Filter.comap` `nhds` `extend`	—	`uniformly_extend_spec` `isUniformInducing_val` `denseRange_val`
`uniformContinuous_extend` 📖	mathematical	`Dense` `UniformSpace.toTopologicalSpace` `UniformContinuous` `Set.Elem` `instUniformSpaceSubtype` `Set` `Set.instMembership`	`extend`	—	`uniformContinuous_uniformly_extend` `isUniformInducing_val` `denseRange_val`

Embedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_isUniformEmbedding` 📖	mathematical	`Topology.IsEmbedding` `UniformSpace.toTopologicalSpace`	`IsUniformEmbedding` `Topology.IsEmbedding.comapUniformSpace`	—	`Topology.IsEmbedding.injective`

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUniformEmbedding` 📖	mathematical	`UniformContinuous` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	`IsUniformEmbedding`	—	`isUniformEmbedding_iff'` `injective` `prodCongr_apply` `Filter.map_equiv_symm`

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`totallyBounded_comap` 📖	mathematical	`IsUniformInducing` `TotallyBounded`	`comap`	—	`totallyBounded_map_iff` `TotallyBounded.mono` `map_comap_le`
`totallyBounded_map_iff` 📖	mathematical	`IsUniformInducing`	`TotallyBounded` `map`	—	`HasBasis.filter_totallyBounded_iff` `IsUniformInducing.basis_uniformity` `basis_sets` `Set.exists_subset_image_finite_and` `TotallyBounded.exists_subset_of_mem` `image_mem_map` `univ_mem` `TotallyBounded.map` `IsUniformInducing.uniformContinuous`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUniformEmbedding_iff` 📖	mathematical	`Filter.HasBasis` `uniformity`	`IsUniformEmbedding` `UniformContinuous` `Set` `Set.instMembership`	—	`isUniformEmbedding_iff'` `uniformContinuous_iff`
`isUniformEmbedding_iff'` 📖	mathematical	`Filter.HasBasis` `uniformity`	`IsUniformEmbedding` `Set` `Set.instMembership`	—	`isUniformEmbedding_iff` `isUniformInducing_iff`
`isUniformInducing_iff` 📖	mathematical	`Filter.HasBasis` `uniformity`	`IsUniformInducing` `Set` `Set.instMembership`	—	`uniformContinuous_iff` `le_basis_iff` `comap`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace_coe` 📖	mathematical	—	`CompleteSpace` `Set.Elem` `instUniformSpaceSubtype` `Set` `Set.instMembership`	—	`IsComplete.completeSpace_coe` `isComplete`

IsComplete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace_coe` 📖	mathematical	`IsComplete`	`CompleteSpace` `Set.Elem` `instUniformSpaceSubtype` `Set` `Set.instMembership`	—	`completeSpace_coe_iff_isComplete`

IsDenseInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUniformInducing_extend` 📖	mathematical	`IsDenseInducing` `UniformSpace.toTopologicalSpace` `IsUniformInducing`	`extend`	—	`IsComplete.completeSpace_coe` `IsClosed.isComplete` `SeparationQuotient.instCompleteSpace` `isClosed_closure` `subset_closure` `IsUniformInducing.comp` `IsUniformEmbedding.isUniformInducing` `isUniformEmbedding_set_inclusion` `IsUniformInducing.rangeFactorization` `DenseRange.comp` `denseRange_inclusion_iff` `subset_rfl` `Set.instReflSubset` `Function.Surjective.denseRange` `Set.rangeFactorization_surjective` `continuous_inclusion` `IsUniformInducing.isDenseInducing` `uniformContinuous_uniformly_extend` `dense` `IsUniformInducing.uniformContinuous` `isClosed_property` `isClosed_eq` `SeparationQuotient.t2Space` `instR1Space` `UniformSpace.to_regularSpace` `Continuous.comp` `UniformContinuous.continuous` `UniformContinuous.comp` `extend.congr_simp` `extend_eq` `instT2SpaceSubtype` `inseparable_extend` `Continuous.continuousAt` `IsUniformInducing.of_comp` `Function.comp_assoc` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Continuous.range_subset_closure_image_dense` `closure_mono` `subset_of_eq` `Set.range_comp` `Set.coe_comp_rangeFactorization` `Set.val_comp_inclusion` `Function.Injective.comp_left` `Subtype.val_injective` `extend_unique` `Continuous.rangeFactorization` `IsUniformInducing.isUniformInducing_comp_iff` `isUniformInducing_val`

IsUniformEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`IsUniformEmbedding`	—	—	`IsUniformInducing.comp` `isUniformInducing` `injective`
`discreteUniformity` 📖	mathematical	`IsUniformEmbedding`	`DiscreteUniformity`	—	`IsUniformInducing.comap_uniformity` `toIsUniformInducing` `DiscreteUniformity.eq_principal_setRelId` `Filter.comap_principal` `injective`
`isComplete_iff` 📖	mathematical	`IsUniformEmbedding`	`IsComplete` `Set.image`	—	`IsUniformInducing.isComplete_iff` `isUniformInducing`
`isDenseEmbedding` 📖	mathematical	`IsUniformEmbedding` `DenseRange` `UniformSpace.toTopologicalSpace`	`IsDenseEmbedding`	—	`isEmbedding` `Topology.IsEmbedding.toIsInducing` `Topology.IsEmbedding.injective`
`isEmbedding` 📖	mathematical	`IsUniformEmbedding`	`Topology.IsEmbedding` `UniformSpace.toTopologicalSpace`	—	`IsUniformInducing.isInducing` `toIsUniformInducing` `injective`
`of_comp_iff` 📖	—	`IsUniformEmbedding`	—	—	`IsUniformInducing.of_comp_iff` `isUniformInducing` `Function.Injective.of_comp_iff` `injective`
`prod` 📖	mathematical	`IsUniformEmbedding`	`instUniformSpaceProd`	—	`IsUniformInducing.prod` `isUniformInducing` `Function.Injective.prodMap` `injective`

IsUniformInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basis_uniformity` 📖	mathematical	`IsUniformInducing` `Filter.HasBasis` `uniformity`	`Set.preimage`	—	`Filter.HasBasis.comap` `comap_uniformity`
`cauchy_map_iff` 📖	mathematical	`IsUniformInducing`	`Cauchy` `Filter.map`	—	`Filter.prod_map_map_eq` `comap_uniformity`
`comap_uniformSpace` 📖	mathematical	`IsUniformInducing`	`UniformSpace.comap`	—	`isUniformInducing_iff_uniformSpace`
`comp` 📖	—	`IsUniformInducing`	—	—	`comap_uniformity` `Filter.comap_comap`
`completeSpace` 📖	mathematical	`IsUniformInducing` `IsComplete` `Set.range`	`CompleteSpace`	—	`completeSpace_iff_isComplete_range`
`completeSpace_congr` 📖	mathematical	`IsUniformInducing`	`CompleteSpace`	—	`completeSpace_iff_isComplete_range` `Function.Surjective.range_eq` `completeSpace_iff_isComplete_univ`
`id` 📖	mathematical	—	`IsUniformInducing`	—	`Prod.map_def` `Filter.comap_id`
`injective` 📖	—	`IsUniformInducing`	—	—	`Topology.IsInducing.injective` `isInducing`
`isComplete_iff` 📖	mathematical	`IsUniformInducing`	`IsComplete` `Set.image`	—	`isComplete_image_iff`
`isComplete_range` 📖	mathematical	`IsUniformInducing`	`IsComplete` `Set.range`	—	`completeSpace_iff_isComplete_range`
`isDenseInducing` 📖	mathematical	`IsUniformInducing` `DenseRange` `UniformSpace.toTopologicalSpace`	`IsDenseInducing`	—	`isInducing`
`isInducing` 📖	mathematical	`IsUniformInducing`	`Topology.IsInducing` `UniformSpace.toTopologicalSpace`	—	`Topology.IsInducing.induced` `comap_uniformSpace`
`isUniformEmbedding` 📖	mathematical	`IsUniformInducing`	`IsUniformEmbedding`	—	`Topology.IsInducing.injective` `isInducing`
`isUniformInducing_comp_iff` 📖	—	`IsUniformInducing`	—	—	`comap_uniformity` `Filter.comap_comap`
`mk'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `uniformity` `Set.instMembership`	`IsUniformInducing`	—	—
`of_comp` 📖	—	`UniformContinuous` `IsUniformInducing`	—	—	`le_antisymm` `comap_uniformity` `Prod.map_def` `Filter.comap_comap` `Filter.comap_mono` `Filter.Tendsto.le_comap`
`of_comp_iff` 📖	—	`IsUniformInducing`	—	—	`isUniformInducing_iff` `comap_uniformity` `Filter.comap_comap` `comp`
`prod` 📖	mathematical	`IsUniformInducing`	`instUniformSpaceProd`	—	`Filter.comap_inf` `Filter.comap_comap` `comap_uniformity`
`rangeFactorization` 📖	mathematical	`IsUniformInducing`	`Set.Elem` `Set.range` `instUniformSpaceSubtype` `Set` `Set.instMembership` `Set.rangeFactorization`	—	`isUniformInducing_rangeFactorization_iff`
`uniformContinuous` 📖	mathematical	`IsUniformInducing`	`UniformContinuous`	—	`isUniformInducing_iff'`
`uniformContinuousOn_iff` 📖	mathematical	`IsUniformInducing`	`UniformContinuousOn`	—	`comap_uniformity` `Filter.map_le_iff_le_comap` `Filter.map_map`
`uniformContinuous_iff` 📖	mathematical	`IsUniformInducing`	`UniformContinuous`	—	`comap_uniformity` `Filter.map_map`

SeparationQuotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace_iff` 📖	mathematical	—	`CompleteSpace` `SeparationQuotient` `UniformSpace.toTopologicalSpace` `instUniformSpace`	—	`IsUniformInducing.completeSpace_congr`
`instCompleteSpace` 📖	mathematical	—	`CompleteSpace` `SeparationQuotient` `UniformSpace.toTopologicalSpace` `instUniformSpace`	—	`completeSpace_iff`
`isUniformInducing_mk` 📖	mathematical	—	`IsUniformInducing` `SeparationQuotient` `UniformSpace.toTopologicalSpace` `instUniformSpace`	—	`comap_mk_uniformity`

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isComplete_iff` 📖	mathematical	—	`IsComplete` `instUniformSpaceSubtype` `Set.image`	—	`IsUniformEmbedding.isComplete_iff` `isUniformEmbedding_subtype_val`

Topology.IsEmbedding

Definitions

Name	Category	Theorems
`comapUniformSpace` 📖	CompOp	1 math math: `Embedding.to_isUniformEmbedding`

ULift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompleteSpace` 📖	mathematical	—	`CompleteSpace` `uniformSpace`	—	`completeSpace_ulift_iff`

UniformContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rangeFactorization` 📖	mathematical	`UniformContinuous`	`Set.Elem` `Set.range` `instUniformSpaceSubtype` `Set` `Set.instMembership` `Set.rangeFactorization`	—	`uniformContinuous_rangeFactorization_iff`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_image_mem_nhds_of_isUniformInducing` 📖	mathematical	`IsUniformInducing` `IsDenseInducing` `UniformSpace.toTopologicalSpace` `Set` `Filter` `Filter.instMembership` `uniformity`	`nhds` `closure` `Set.image` `setOf` `Set.instMembership`	—	`Filter.HasBasis.mem_iff` `Filter.HasBasis.comap` `uniformity_hasBasis_open_symmetric` `IsUniformInducing.comap_uniformity` `DenseRange.mem_nhds` `IsDenseInducing.dense` `UniformSpace.ball_mem_nhds` `Filter.mem_of_superset` `UniformSpace.isOpen_ball` `IsOpen.mem_nhds` `UniformSpace.mem_ball_symmetry` `mem_closure_iff_nhds` `Filter.inter_mem` `Set.mem_image_of_mem` `closure_mono` `Set.image_mono` `UniformSpace.ball_mono`
`comap_uniformity_of_spaced_out` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `uniformity` `Pairwise` `Set.instMembership`	`Filter.comap` `Filter.principal` `SetRel.id`	—	`le_antisymm` `Filter.comap_mono` `Filter.le_principal_iff` `Filter.comap_principal` `Filter.principal_mono` `refl_le_uniformity`
`completeSpace_coe_iff_isComplete` 📖	mathematical	—	`CompleteSpace` `Set.Elem` `instUniformSpaceSubtype` `Set` `Set.instMembership` `IsComplete`	—	`completeSpace_iff_isComplete_range` `IsUniformEmbedding.isUniformInducing` `isUniformEmbedding_subtype_val` `Subtype.range_coe`
`completeSpace_congr` 📖	mathematical	`IsUniformEmbedding` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`CompleteSpace`	—	`IsUniformInducing.completeSpace_congr` `IsUniformEmbedding.toIsUniformInducing` `Equiv.surjective`
`completeSpace_extension` 📖	mathematical	`IsUniformInducing` `DenseRange` `UniformSpace.toTopologicalSpace` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.map` `nhds`	`CompleteSpace`	—	`le_iInf₂` `Filter.le_principal_iff` `Filter.mem_of_superset` `refl_mem_uniformity` `Filter.NeBot.mono` `Filter.comap_neBot` `Filter.mem_lift_sets` `Filter.monotone_lift'` `monotone_const` `Filter.mem_lift'_sets` `Filter.NeBot.nonempty_of_mem` `DenseRange.nhdsWithin_neBot` `Filter.mem_inf_of_left` `mem_nhds_left` `Filter.mem_inf_of_right` `Set.Subset.refl` `Filter.inter_mem` `comp_mem_uniformity_sets` `Filter.mem_prod_same_iff` `Filter.mem_lift` `symm_le_uniformity` `Filter.mem_lift'` `Filter.prod_mem_prod` `Filter.sets_of_superset` `SetRel.prodMk_mem_comp` `Cauchy.comap'` `le_of_eq` `IsUniformInducing.comap_uniformity` `le_nhds_iff_adhp_of_cauchy` `Cauchy.map` `IsUniformInducing.uniformContinuous` `ClusterPt.mono` `Filter.map_comap_le` `le_nhds_of_cauchy_adhp`
`completeSpace_iff_isComplete_range` 📖	mathematical	`IsUniformInducing`	`CompleteSpace` `IsComplete` `Set.range`	—	`completeSpace_iff_isComplete_univ` `isComplete_image_iff` `Set.image_univ`
`completeSpace_ulift_iff` 📖	mathematical	—	`CompleteSpace` `ULift.uniformSpace`	—	`IsUniformInducing.completeSpace_congr` `ULift.down_surjective`
`isClosedEmbedding_of_spaced_out` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `uniformity` `Pairwise` `Set.instMembership`	`Topology.IsClosedEmbedding` `UniformSpace.toTopologicalSpace`	—	`IsUniformEmbedding.isEmbedding` `isUniformEmbedding_of_spaced_out` `isClosed_range_of_spaced_out` `DiscreteTopology.eq_bot`
`isComplete_image_iff` 📖	mathematical	`IsUniformInducing`	`IsComplete` `Set.image`	—	`Set.SurjOn.filter_map_Iic` `Set.surjOn_image` `Set.MapsTo.filter_map_Iic` `Set.mapsTo_image` `Set.mem_Iic` `Set.SurjOn.forall` `IsUniformInducing.cauchy_map_iff` `Topology.IsInducing.nhds_eq_comap` `IsUniformInducing.isInducing`
`isComplete_of_complete_image` 📖	—	`IsUniformInducing` `IsComplete` `Set.image`	—	—	`isComplete_image_iff`
`isUniformEmbedding_comap` 📖	mathematical	—	`IsUniformEmbedding` `UniformSpace.comap`	—	—
`isUniformEmbedding_iff'` 📖	mathematical	—	`IsUniformEmbedding` `UniformContinuous` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.comap` `uniformity`	—	`isUniformEmbedding_iff` `isUniformInducing_iff'`
`isUniformEmbedding_iff_isUniformInducing` 📖	mathematical	—	`IsUniformEmbedding` `IsUniformInducing`	—	`IsUniformEmbedding.isUniformInducing` `IsUniformInducing.isUniformEmbedding`
`isUniformEmbedding_inl` 📖	mathematical	—	`IsUniformEmbedding` `Sum.instUniformSpace`	—	`isUniformEmbedding_iff'` `Sum.inl_injective` `uniformContinuous_inl` `Filter.union_mem_sup` `Filter.image_mem_map` `Filter.range_mem_map` `Set.image_congr` `Set.range_prodMap`
`isUniformEmbedding_inr` 📖	mathematical	—	`IsUniformEmbedding` `Sum.instUniformSpace`	—	`isUniformEmbedding_iff'` `Sum.inr_injective` `uniformContinuous_inr` `Filter.union_mem_sup` `Filter.range_mem_map` `Filter.image_mem_map` `Set.range_prodMap` `Set.image_congr`
`isUniformEmbedding_of_spaced_out` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `uniformity` `Pairwise` `Set.instMembership`	`IsUniformEmbedding` `Bot.bot` `UniformSpace` `instBotUniformSpace`	—	`discreteTopology_bot` `IsUniformInducing.isUniformEmbedding` `T1Space.t0Space` `T2Space.t1Space` `DiscreteTopology.toT2Space` `comap_uniformity_of_spaced_out`
`isUniformEmbedding_set_inclusion` 📖	mathematical	`Set` `Set.instHasSubset`	`IsUniformEmbedding` `Set.Elem` `instUniformSpaceSubtype` `Set.instMembership` `Set.inclusion`	—	`uniformity_subtype` `Filter.comap_comap` `Set.inclusion_injective`
`isUniformEmbedding_subtypeEmb` 📖	mathematical	`IsUniformEmbedding` `IsDenseEmbedding` `UniformSpace.toTopologicalSpace`	`Set` `Set.instMembership` `closure` `Set.image` `setOf` `instUniformSpaceSubtype` `IsDenseEmbedding.subtypeEmb`	—	`Filter.comap_comap` `IsUniformInducing.comap_uniformity` `IsUniformEmbedding.toIsUniformInducing` `IsDenseEmbedding.injective` `IsDenseEmbedding.subtype`
`isUniformEmbedding_subtype_val` 📖	mathematical	—	`IsUniformEmbedding` `instUniformSpaceSubtype`	—	`Subtype.val_injective`
`isUniformInducing_iff'` 📖	mathematical	—	`IsUniformInducing` `UniformContinuous` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.comap` `uniformity`	—	`isUniformInducing_iff` `UniformContinuous.eq_1` `Filter.tendsto_iff_comap` `le_antisymm_iff`
`isUniformInducing_iff_uniformSpace` 📖	mathematical	—	`IsUniformInducing` `UniformSpace.comap`	—	`isUniformInducing_iff` `UniformSpace.ext_iff` `Filter.ext_iff`
`isUniformInducing_rangeFactorization_iff` 📖	mathematical	—	`IsUniformInducing` `Set.Elem` `Set.range` `instUniformSpaceSubtype` `Set` `Set.instMembership` `Set.rangeFactorization`	—	`IsUniformInducing.isUniformInducing_comp_iff` `isUniformInducing_val`
`isUniformInducing_val` 📖	mathematical	—	`IsUniformInducing` `instUniformSpaceSubtype`	—	`uniformity_setCoe`
`totallyBounded_image_iff` 📖	mathematical	`IsUniformInducing`	`TotallyBounded` `Set.image`	—	`Filter.totallyBounded_map_iff`
`totallyBounded_preimage` 📖	mathematical	`IsUniformInducing` `TotallyBounded`	`Set.preimage`	—	`totallyBounded_image_iff` `TotallyBounded.subset` `Set.image_preimage_subset`
`uniformContinuous_rangeFactorization_iff` 📖	mathematical	—	`UniformContinuous` `Set.Elem` `Set.range` `instUniformSpaceSubtype` `Set` `Set.instMembership` `Set.rangeFactorization`	—	`IsUniformInducing.uniformContinuous_iff` `isUniformInducing_val`
`uniformContinuous_uniformly_extend` 📖	mathematical	`IsUniformInducing` `DenseRange` `UniformSpace.toTopologicalSpace` `UniformContinuous`	`IsDenseInducing.extend` `IsUniformInducing.isDenseInducing`	—	`IsUniformInducing.isDenseInducing` `comp3_mem_uniformity` `Filter.NeBot.map` `IsDenseInducing.comap_nhds_neBot` `Filter.inter_mem` `Filter.image_mem_map` `Filter.preimage_mem_comap` `uniformly_extend_spec` `mem_nhds_right` `mem_nhds_left` `Filter.NeBot.nonempty_of_mem` `IsUniformInducing.comap_uniformity` `Filter.mem_of_superset` `interior_mem_uniformity` `IsOpen.mem_nhds` `isOpen_interior` `mem_nhds_prod_iff` `Set.mem_preimage` `interior_subset`
`uniform_extend_subtype` 📖	mathematical	`UniformContinuous` `instUniformSpaceSubtype` `IsUniformEmbedding` `Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `Set.range` `Filter` `Filter.instMembership` `nhds` `Set.image`	`Filter.Tendsto` `Filter.comap`	—	`IsUniformEmbedding.isDenseEmbedding` `IsDenseEmbedding.subtype` `isUniformEmbedding_subtypeEmb` `closure_mono` `Set.monotone_image` `mem_of_mem_nhds` `uniformly_extend_exists` `IsUniformEmbedding.isUniformInducing` `IsDenseInducing.dense` `IsDenseEmbedding.toIsDenseInducing` `Filter.comap_comap` `nhds_subtype_eq_comap` `Filter.tendsto_comap'_iff` `Subtype.range_coe_subtype` `Topology.IsInducing.closure_eq_preimage_closure_image` `IsDenseInducing.isInducing` `IsClosed.closure_eq`
`uniformly_extend_exists` 📖	mathematical	`IsUniformInducing` `DenseRange` `UniformSpace.toTopologicalSpace` `UniformContinuous`	`Filter.Tendsto` `Filter.comap` `nhds`	—	`IsUniformInducing.isDenseInducing` `cauchy_nhds` `Cauchy.comap'` `le_of_eq` `IsUniformInducing.comap_uniformity` `IsDenseInducing.comap_nhds_neBot` `Cauchy.map` `CompleteSpace.complete`
`uniformly_extend_of_ind` 📖	mathematical	`IsUniformInducing` `DenseRange` `UniformSpace.toTopologicalSpace` `UniformContinuous`	`IsDenseInducing.extend` `IsUniformInducing.isDenseInducing`	—	`IsDenseInducing.extend_eq_at` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `UniformSpace.to_regularSpace` `IsUniformInducing.isDenseInducing` `Continuous.continuousAt` `UniformContinuous.continuous`
`uniformly_extend_spec` 📖	mathematical	`IsUniformInducing` `DenseRange` `UniformSpace.toTopologicalSpace` `UniformContinuous`	`Filter.Tendsto` `Filter.comap` `nhds` `IsDenseInducing.extend` `IsUniformInducing.isDenseInducing`	—	`IsUniformInducing.isDenseInducing` `tendsto_nhds_limUnder` `uniformly_extend_exists`
`uniformly_extend_unique` 📖	mathematical	`IsUniformInducing` `DenseRange` `UniformSpace.toTopologicalSpace` `Continuous`	`IsDenseInducing.extend` `IsUniformInducing.isDenseInducing`	—	`IsDenseInducing.extend_unique` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `UniformSpace.to_regularSpace` `IsUniformInducing.isDenseInducing`

---

← Back to Index