Basic

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

Statistics

Metric	Count
Definitions instUniformSpace, instUniformSpace, uniformSpace, UniformContinuous₂, comap, entourageProd, inhabitedUniformSpace, inhabitedUniformSpaceCore, instBotUniformSpace, instCompleteLatticeUniformSpace, instInfSetUniformSpace, instMinUniformSpace, instPartialOrderUniformSpace, instTopUniformSpace, instUniformSpaceAddOpposite, instUniformSpaceAdditive, instUniformSpaceBool, instUniformSpaceEmpty, instUniformSpaceInt, instUniformSpaceMulOpposite, instUniformSpaceMultiplicative, instUniformSpaceNat, instUniformSpacePUnit, instUniformSpaceProd, instUniformSpaceSubtype, instUniqueUniformSpaceOfSubsingleton	26
Theorems uniformContinuous_op, uniformContinuous_unop, biUnion_uniformity_ball, iUnion_uniformity_ball, mem_uniformity_iff, uniformSpace_eq_bot, uniformity_closure, uniformity_prod, congr_uniformity, relImage_of_finite, relInv, relPreimage_of_finite, relComp, relImage, relInv, relPreimage, IsSymm_entourageProd, uniformContinuous_op, uniformContinuous_unop, uniformity, continuousAt_iff'_left, continuousAt_iff'_right, continuousAt_iff_prod, continuousOn_iff'_left, continuousOn_iff'_right, continuousWithinAt_iff'_left, continuousWithinAt_iff'_right, continuous_iff'_left, continuous_iff'_right, exists_is_open_mem_uniformity_of_forall_mem_eq, tendsto_congr, tendsto_nhds_left, tendsto_nhds_right, comp_uniformContinuousOn, continuous, inf_dom_left, inf_dom_right, inf_rng, prodMap, prodMk, prodMk_left, prodMk_right, subtype_map, subtype_mk, uniformContinuousOn, comp, continuousOn, mono, bicompl, comp, uniformContinuous, comap_comap, comap_iInf, comap_inf, comap_mono, hasBasis_nhds_prod, has_seq_basis, isClosed_ball, isOpen_ball, le_def, le_sInf, sInf_le, toTopologicalSpace_bot, toTopologicalSpace_comap, toTopologicalSpace_iInf, toTopologicalSpace_inf, toTopologicalSpace_mono, toTopologicalSpace_sInf, toTopologicalSpace_top, to_nhds_mono, uniformSpace_eq_bot, ball_entourageProd, ball_preimage, bot_uniformity, closure_ball_subset, closure_eq_inter_uniformity, closure_eq_uniformity, comap_uniformity_addOpposite, comap_uniformity_mulOpposite, comp_open_symm_mem_uniformity_sets, discreteTopology_of_discrete_uniformity, entourageProd_mem_uniformity, entourageProd_subset, eventually_uniformity_comp_subset, eventually_uniformity_iterate_comp_subset, iInf_uniformity, iSup_nhds_le_uniformity, image_entourageProd_prod, inf_uniformity, instIsCountablyGeneratedProdElemUniformity, instIsCountablyGeneratedProdSumUniformity, instIsCountablyGeneratedProdUniformity, interior_mem_uniformity, inv_entourageProd, isOpen_iff_isOpen_ball_subset, le_iff_uniformContinuous_id, map_uniformity_set_coe, mem_entourageProd, mem_uniformity_isClosed, mem_uniformity_of_uniformContinuous_invariant, nhdsSet_diagonal_le_uniformity, nhds_eq_uniformity_prod, nhds_le_uniformity, nhdset_of_mem_uniformity, preimage_entourageProd_prod, tendsto_of_uniformContinuous_subtype, tendsto_prod_uniformity_fst, tendsto_prod_uniformity_snd, toTopologicalSpace_prod, toTopologicalSpace_subtype, top_uniformity, uniformContinuousOn_iff_restrict, uniformContinuous_comap, uniformContinuous_comap', uniformContinuous_fst, uniformContinuous_iInf_dom, uniformContinuous_iInf_rng, uniformContinuous_iff, uniformContinuous_inf_dom_left₂, uniformContinuous_inf_dom_right₂, uniformContinuous_inl, uniformContinuous_inr, uniformContinuous_ofAdd, uniformContinuous_ofMul, uniformContinuous_sInf_dom, uniformContinuous_sInf_dom₂, uniformContinuous_sInf_rng, uniformContinuous_snd, uniformContinuous_subtype_val, uniformContinuous_swap, uniformContinuous_toAdd, uniformContinuous_toMul, uniformContinuous₂_curry, uniformContinuous₂_def, uniformSpace_comap_id, uniformity_addOpposite, uniformity_additive, uniformity_comap, uniformity_eq_uniformity_closure, uniformity_eq_uniformity_interior, uniformity_hasBasis_closed, uniformity_hasBasis_closure, uniformity_hasBasis_open, uniformity_hasBasis_open_symmetric, uniformity_mulOpposite, uniformity_multiplicative, uniformity_prod, uniformity_prod_eq_comap_prod, uniformity_prod_eq_prod, uniformity_setCoe, uniformity_subtype, union_mem_uniformity_sum	152
Total	178

AddOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformContinuous_op 📖	mathematical	—	UniformContinuous AddOpposite instUniformSpaceAddOpposite op	—	uniformContinuous_comap' uniformContinuous_id
uniformContinuous_unop 📖	mathematical	—	UniformContinuous AddOpposite instUniformSpaceAddOpposite unop	—	uniformContinuous_comap

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biUnion_uniformity_ball 📖	mathematical	Dense UniformSpace.toTopologicalSpace SetRel Filter Filter.instMembership uniformity	Set.iUnion Set Set.instMembership UniformSpace.ball Set.univ	—	Set.iUnion₂_eq_univ_iff inter_nhds_nonempty mem_nhds_right

DenseRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iUnion_uniformity_ball 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace SetRel Filter Filter.instMembership uniformity	Set.iUnion UniformSpace.ball Set.univ	—	Set.biUnion_range Dense.biUnion_uniformity_ball

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_uniformity_iff 📖	mathematical	Filter.HasBasis uniformity	SetRel Filter Filter.instMembership Set.instMembership	—	mem_iff
uniformSpace_eq_bot 📖	mathematical	Filter.HasBasis uniformity	Bot.bot UniformSpace instBotUniformSpace Pairwise SetRel Set.instMembership	—	mem_iff
uniformity_closure 📖	mathematical	Filter.HasBasis uniformity	closure instTopologicalSpaceProd UniformSpace.toTopologicalSpace	—	lift'_closure uniformity_eq_uniformity_closure
uniformity_prod 📖	mathematical	Filter.HasBasis uniformity	instUniformSpaceProd entourageProd	—	inf comap

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_uniformity 📖	—	Filter.Tendsto nhds UniformSpace.toTopologicalSpace uniformity	—	—	Uniform.tendsto_nhds_right uniformity_trans

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
relImage_of_finite 📖	mathematical	—	IsClosed SetRel.image	—	Set.setOf_exists Set.Finite.isClosed_biUnion preimage Continuous.prodMk_right
relInv 📖	mathematical	—	IsClosed instTopologicalSpaceProd SetRel.inv	—	preimage continuous_swap
relPreimage_of_finite 📖	mathematical	—	IsClosed SetRel.preimage	—	relImage_of_finite relInv

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
relComp 📖	mathematical	IsOpen instTopologicalSpaceProd	SetRel.comp	—	Set.ext isOpen_iUnion inter preimage Continuous.prodMk Continuous.fst continuous_id' continuous_const Continuous.snd
relImage 📖	mathematical	IsOpen instTopologicalSpaceProd	SetRel.image	—	Set.setOf_exists isOpen_biUnion preimage Continuous.prodMk_right
relInv 📖	mathematical	IsOpen instTopologicalSpaceProd	SetRel.inv	—	preimage continuous_swap
relPreimage 📖	mathematical	IsOpen instTopologicalSpaceProd	SetRel.preimage	—	relImage relInv

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformContinuous_op 📖	mathematical	—	UniformContinuous MulOpposite instUniformSpaceMulOpposite op	—	uniformContinuous_comap' uniformContinuous_id
uniformContinuous_unop 📖	mathematical	—	UniformContinuous MulOpposite instUniformSpaceMulOpposite unop	—	uniformContinuous_comap

OrderDual

Definitions

Name	Category	Theorems
instUniformSpace 📖	CompOp	—

Sum

Definitions

Name	Category	Theorems
instUniformSpace 📖	CompOp	9 math math: isUniformEmbedding_inl, isUniformEmbedding_inr, instIsCountablyGeneratedProdSumUniformity, uniformContinuous_inr, CompleteSpace.sum, Metric.Sum.mem_uniformity_iff_glueDist, uniformity, uniformContinuous_inl, union_mem_uniformity_sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformity 📖	mathematical	—	uniformity instUniformSpace Filter Filter.instSup Filter.map	—	—

ULift

Definitions

Name	Category	Theorems
uniformSpace 📖	CompOp	2 math math: instCompleteSpace, completeSpace_ulift_iff

Uniform

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt_iff'_left 📖	mathematical	—	ContinuousAt UniformSpace.toTopologicalSpace Filter.Tendsto nhds uniformity	—	ContinuousAt.eq_1 tendsto_nhds_left
continuousAt_iff'_right 📖	mathematical	—	ContinuousAt UniformSpace.toTopologicalSpace Filter.Tendsto nhds uniformity	—	ContinuousAt.eq_1 tendsto_nhds_right
continuousAt_iff_prod 📖	mathematical	—	ContinuousAt UniformSpace.toTopologicalSpace Filter.Tendsto nhds instTopologicalSpaceProd uniformity	—	le_trans ContinuousAt.prodMap' nhds_le_uniformity continuousAt_iff'_left Filter.Tendsto.comp Filter.Tendsto.prodMk_nhds Filter.tendsto_id tendsto_const_nhds
continuousOn_iff'_left 📖	mathematical	—	ContinuousOn UniformSpace.toTopologicalSpace Filter.Tendsto nhdsWithin uniformity	—	—
continuousOn_iff'_right 📖	mathematical	—	ContinuousOn UniformSpace.toTopologicalSpace Filter.Tendsto nhdsWithin uniformity	—	—
continuousWithinAt_iff'_left 📖	mathematical	—	ContinuousWithinAt UniformSpace.toTopologicalSpace Filter.Tendsto nhdsWithin uniformity	—	ContinuousWithinAt.eq_1 tendsto_nhds_left
continuousWithinAt_iff'_right 📖	mathematical	—	ContinuousWithinAt UniformSpace.toTopologicalSpace Filter.Tendsto nhdsWithin uniformity	—	ContinuousWithinAt.eq_1 tendsto_nhds_right
continuous_iff'_left 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace Filter.Tendsto nhds uniformity	—	continuous_iff_continuousAt tendsto_nhds_left
continuous_iff'_right 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace Filter.Tendsto nhds uniformity	—	continuous_iff_continuousAt tendsto_nhds_right
exists_is_open_mem_uniformity_of_forall_mem_eq 📖	mathematical	ContinuousAt UniformSpace.toTopologicalSpace Set.EqOn SetRel Filter Filter.instMembership uniformity	IsOpen Set Set.instHasSubset Set.instMembership	—	comp_symm_mem_uniformity_sets ContinuousAt.preimage_mem_nhds mem_nhds_left mem_nhds_iff Filter.inter_mem SetRel.symm SetRel.prodMk_mem_comp isOpen_biUnion Set.mem_biUnion Function.sometimes_spec
tendsto_congr 📖	mathematical	Filter.Tendsto uniformity	nhds UniformSpace.toTopologicalSpace	—	Filter.Tendsto.congr_uniformity Filter.Tendsto.uniformity_symm
tendsto_nhds_left 📖	mathematical	—	Filter.Tendsto nhds UniformSpace.toTopologicalSpace uniformity	—	nhds_eq_comap_uniformity' Filter.tendsto_comap_iff
tendsto_nhds_right 📖	mathematical	—	Filter.Tendsto nhds UniformSpace.toTopologicalSpace uniformity	—	nhds_eq_comap_uniformity Filter.tendsto_comap_iff

UniformContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_uniformContinuousOn 📖	—	UniformContinuous UniformContinuousOn	—	—	UniformContinuousOn.comp uniformContinuousOn Set.mapsTo_univ
continuous 📖	mathematical	UniformContinuous	Continuous UniformSpace.toTopologicalSpace	—	continuous_iff_le_induced UniformSpace.toTopologicalSpace_mono uniformContinuous_iff
inf_dom_left 📖	mathematical	UniformContinuous	UniformSpace instMinUniformSpace	—	Filter.tendsto_inf_left
inf_dom_right 📖	mathematical	UniformContinuous	UniformSpace instMinUniformSpace	—	Filter.tendsto_inf_right
inf_rng 📖	mathematical	UniformContinuous	UniformSpace instMinUniformSpace	—	Filter.tendsto_inf
prodMap 📖	mathematical	UniformContinuous	instUniformSpaceProd	—	prodMk comp uniformContinuous_fst uniformContinuous_snd
prodMk 📖	mathematical	UniformContinuous	instUniformSpaceProd	—	eq_1 uniformity_prod Filter.tendsto_inf Filter.tendsto_comap_iff
prodMk_left 📖	—	UniformContinuous instUniformSpaceProd	—	—	comp prodMk uniformContinuous_id uniformContinuous_const
prodMk_right 📖	—	UniformContinuous instUniformSpaceProd	—	—	comp prodMk uniformContinuous_const uniformContinuous_id
subtype_map 📖	mathematical	UniformContinuous	instUniformSpaceSubtype Subtype.map	—	comp uniformContinuous_subtype_val
subtype_mk 📖	mathematical	UniformContinuous	instUniformSpaceSubtype	—	uniformContinuous_comap'
uniformContinuousOn 📖	mathematical	UniformContinuous	UniformContinuousOn	—	Filter.tendsto_inf_left

UniformContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	UniformContinuousOn Set.MapsTo	—	—	Filter.Tendsto.comp Filter.tendsto_inf Filter.tendsto_inf_right
continuousOn 📖	mathematical	UniformContinuousOn	ContinuousOn UniformSpace.toTopologicalSpace	—	continuousOn_iff_continuous_restrict UniformContinuous.continuous uniformContinuousOn_iff_restrict
mono 📖	—	UniformContinuousOn Set Set.instHasSubset	—	—	Filter.Tendsto.mono_left inf_le_inf le_rfl

UniformContinuous₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bicompl 📖	mathematical	UniformContinuous₂ UniformContinuous	Function.bicompl	—	UniformContinuous.comp uniformContinuous UniformContinuous.prodMap
comp 📖	mathematical	UniformContinuous UniformContinuous₂	Function.bicompr	—	UniformContinuous.comp
uniformContinuous 📖	mathematical	UniformContinuous₂	UniformContinuous instUniformSpaceProd	—	—

UniformSpace

Definitions

Name	Category	Theorems
comap 📖	CompOp	48 math math: Pi.uniformSpace_eq, Dynamics.coverEntropyInf_image_of_comap, AddOpposite.comap_op_leftUniformSpace, isUniformEmbedding_comap, IsUniformInducing.comap_uniformSpace, UniformFun.uniformSpace_eq_iInf_precomp_of_cover, comap_inv_leftUniformSpace, Pi.uniformSpace_comap_precomp, toTopologicalSpace_comap, WithAbs.uniformSpace_comap_eq_of_comp, Pi.uniformSpace_comap_restrict, Pi.uniformSpace_comap_precomp', cauchy_comap_uniformSpace, comap_neg_leftUniformSpace, ContDiffMapSupportedIn.uniformSpace_eq_iInf, Equicontinuous.comap_uniformFun_eq, comap_inf, UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover, IsUniformGroup.comap, isUniformInducing_iff_uniformSpace, UniformEquiv.comap_eq, comap_comap, uniformContinuous_comap', EquicontinuousOn.comap_uniformOnFun_eq, comap_mono, IsUniformAddGroup.comap, uniformContinuous_iff, MulOpposite.comap_op_leftUniformSpace, comap_iInf, uniformContinuous_comap, Pi.uniformSpace_comap_restrict_sUnion, UniformConvergenceCLM.uniformSpace_eq, uniformity_eq_of_bilipschitz, UniformOnFun.uniformSpace_eq_inf_precomp_of_cover, MulOpposite.comap_op_rightUniformSpace, Dynamics.coverEntropy_image_of_comap, UniformFun.comap_eq, Unitization.uniformity_eq_aux, uniformity_comap, ContinuousMap.uniformSpace_eq_iInf_precomp_of_cover, UniformOnFun.hasBasis_uniformity_of_basis_aux₁, UniformFun.uniformSpace_eq_inf_precomp_of_cover, UniformOnFun.comap_eq, UniformOnFun.hasBasis_uniformity_of_basis_aux₂, AddOpposite.comap_op_rightUniformSpace, uniformSpace_comap_id, IsUltraUniformity.comap, ContinuousMap.uniformSpace_eq_inf_precomp_of_cover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_comap 📖	mathematical	—	comap	—	ext Filter.comap_comap
comap_iInf 📖	mathematical	—	comap iInf UniformSpace instInfSetUniformSpace	—	ext iInf_uniformity Filter.comap_iInf
comap_inf 📖	mathematical	—	comap UniformSpace instMinUniformSpace	—	ext Filter.comap_inf
comap_mono 📖	mathematical	—	Monotone UniformSpace PartialOrder.toPreorder instPartialOrderUniformSpace comap	—	Filter.comap_mono
hasBasis_nhds_prod 📖	mathematical	—	Filter.HasBasis Set nhds instTopologicalSpaceProd toTopologicalSpace Filter Filter.instMembership uniformity SetRel.IsSymm SProd.sprod Set.instSProd ball	—	nhds_prod_eq Filter.HasBasis.prod_same_index hasBasis_nhds Filter.inter_sets SetRel.isSymm_inter ball_inter_left ball_inter_right
has_seq_basis 📖	mathematical	—	Filter.HasAntitoneBasis Nat.instPreorder uniformity SetRel.IsSymm	—	Filter.HasBasis.exists_antitone_subbasis hasBasis_symmetric
isClosed_ball 📖	mathematical	—	IsClosed toTopologicalSpace ball	—	IsClosed.preimage Continuous.prodMk_right
isOpen_ball 📖	mathematical	IsOpen instTopologicalSpaceProd toTopologicalSpace	ball	—	IsOpen.preimage Continuous.prodMk_right
le_def 📖	mathematical	—	UniformSpace Preorder.toLE PartialOrder.toPreorder instPartialOrderUniformSpace Filter Filter.instPartialOrder uniformity	—	—
le_sInf 📖	mathematical	UniformSpace Preorder.toLE PartialOrder.toPreorder instPartialOrderUniformSpace	InfSet.sInf instInfSetUniformSpace	—	le_iInf₂
sInf_le 📖	mathematical	UniformSpace Set Set.instMembership	Preorder.toLE PartialOrder.toPreorder instPartialOrderUniformSpace InfSet.sInf instInfSetUniformSpace	—	iInf₂_le
toTopologicalSpace_bot 📖	mathematical	—	toTopologicalSpace Bot.bot UniformSpace instBotUniformSpace TopologicalSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
toTopologicalSpace_comap 📖	mathematical	—	toTopologicalSpace comap TopologicalSpace.induced	—	—
toTopologicalSpace_iInf 📖	mathematical	—	toTopologicalSpace iInf UniformSpace instInfSetUniformSpace TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	TopologicalSpace.ext_nhds nhds_eq_comap_uniformity iInf_uniformity Filter.comap_iInf nhds_iInf
toTopologicalSpace_inf 📖	mathematical	—	toTopologicalSpace UniformSpace instMinUniformSpace TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	—
toTopologicalSpace_mono 📖	mathematical	UniformSpace Preorder.toLE PartialOrder.toPreorder instPartialOrderUniformSpace	TopologicalSpace TopologicalSpace.instPartialOrder toTopologicalSpace	—	le_of_nhds_le_nhds to_nhds_mono
toTopologicalSpace_sInf 📖	mathematical	—	toTopologicalSpace InfSet.sInf UniformSpace instInfSetUniformSpace iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Set Set.instMembership	—	sInf_eq_iInf
toTopologicalSpace_top 📖	mathematical	—	toTopologicalSpace Top.top UniformSpace instTopUniformSpace TopologicalSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
to_nhds_mono 📖	mathematical	UniformSpace Preorder.toLE PartialOrder.toPreorder instPartialOrderUniformSpace	Filter Filter.instPartialOrder nhds toTopologicalSpace	—	nhds_eq_uniformity Filter.lift'_mono le_rfl
uniformSpace_eq_bot 📖	mathematical	—	Bot.bot UniformSpace instBotUniformSpace SetRel Filter Filter.instMembership uniformity SetRel.id	—	le_bot_iff Filter.le_principal_iff

(root)

Definitions

Name	Category	Theorems
UniformContinuous₂ 📖	MathDef	6 math math: AbstractCompletion.uniformContinuous_map₂, UniformSpace.Completion.uniformContinuous_extension₂, uniformContinuous₂_def, uniformContinuous₂_curry, UniformSpace.Completion.uniformContinuous_map₂, AbstractCompletion.uniformContinuous_extension₂
entourageProd 📖	CompOp	11 math math: Filter.HasBasis.uniformity_prod, ball_entourageProd, entourageProd_subset, SetRel.isTrans_entourageProd, entourageProd_mem_uniformity, mem_entourageProd, IsTransitiveRel.entourageProd, preimage_entourageProd_prod, IsSymm_entourageProd, inv_entourageProd, image_entourageProd_prod
inhabitedUniformSpace 📖	CompOp	—
inhabitedUniformSpaceCore 📖	CompOp	—
instBotUniformSpace 📖	CompOp	10 math math: bot_uniformity, DiscreteUniformity.eq_bot, UniformSpace.toTopologicalSpace_bot, isUniformEmbedding_of_spaced_out, discreteUniformity_iff_eq_bot, UniformSpace.uniformSpace_eq_bot, Metric.isUniformEmbedding_bot_of_pairwise_le_dist, DiscreteUniformity.inst, Metric.uniformSpace_eq_bot, Filter.HasBasis.uniformSpace_eq_bot
instCompleteLatticeUniformSpace 📖	CompOp	—
instInfSetUniformSpace 📖	CompOp	39 math math: Pi.uniformSpace_eq, uniformContinuous_sInf_rng, uniformContinuous_sInf_dom, UniformFun.uniformSpace_eq_iInf_precomp_of_cover, Pi.uniformSpace_comap_precomp, isUniformAddGroup_sInf, cauchy_iInf_uniformSpace', Pi.uniformSpace_comap_restrict, uniformEquicontinuousOn_iInf_rng, Pi.uniformSpace_comap_precomp', uniformEquicontinuous_iInf_rng, UniformSpace.sInf_le, ContDiffMapSupportedIn.uniformSpace_eq_iInf, equicontinuous_iInf_rng, uniformEquicontinuousOn_iInf_dom, UniformSpace.le_sInf, UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover, SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf, iInf_uniformity, isUniformGroup_sInf, UniformSpace.toTopologicalSpace_sInf, uniformContinuous_sInf_dom₂, equicontinuousOn_iInf_rng, IsUltraUniformity.iInf, UniformSpace.toTopologicalSpace_iInf, CompleteSpace.iInf, isUniformAddGroup_iInf, uniformEquicontinuous_iInf_dom, isUniformGroup_iInf, UniformSpace.comap_iInf, Pi.uniformSpace_comap_restrict_sUnion, equicontinuousWithinAt_iInf_rng, uniformContinuous_iInf_rng, UniformFun.iInf_eq, cauchy_iInf_uniformSpace, ContinuousMap.uniformSpace_eq_iInf_precomp_of_cover, equicontinuousAt_iInf_rng, uniformContinuous_iInf_dom, UniformOnFun.iInf_eq
instMinUniformSpace 📖	CompOp	17 math math: cauchy_inf_uniformSpace, isUniformGroup_inf, isUniformAddGroup_inf, uniformContinuous_inf_dom_left₂, UniformContinuous.inf_dom_left, uniformContinuous_inf_dom_right₂, UniformSpace.comap_inf, UniformContinuous.inf_dom_right, IsUltraUniformity.inf, inf_uniformity, UniformOnFun.inf_eq, UniformSpace.toTopologicalSpace_inf, UniformOnFun.uniformSpace_eq_inf_precomp_of_cover, UniformFun.uniformSpace_eq_inf_precomp_of_cover, UniformFun.inf_eq, UniformContinuous.inf_rng, ContinuousMap.uniformSpace_eq_inf_precomp_of_cover
instPartialOrderUniformSpace 📖	CompOp	10 math math: UniformFun.mono, UniformSpace.sInf_le, UniformConvergenceCLM.uniformSpace_mono, le_iff_uniformContinuous_id, Dynamics.coverEntropy_antitone, Dynamics.coverEntropyInf_antitone, UniformSpace.comap_mono, UniformSpace.le_def, uniformContinuous_iff, UniformOnFun.hasBasis_uniformity_of_basis_aux₂
instTopUniformSpace 📖	CompOp	3 math math: UniformSpace.toTopologicalSpace_top, IsUltraUniformity.top, top_uniformity
instUniformSpaceAddOpposite 📖	CompOp	7 math math: comap_uniformity_addOpposite, CompleteSpace.addOpposite, AddOpposite.uniformContinuous_unop, AddOpposite.uniformContinuous_op, AddOpposite.uniformContinuousConstVAdd, AddOpposite.instIsUniformAddGroup, uniformity_addOpposite
instUniformSpaceAdditive 📖	CompOp	3 math math: uniformContinuous_toMul, uniformContinuous_ofMul, uniformity_additive
instUniformSpaceBool 📖	CompOp	—
instUniformSpaceEmpty 📖	CompOp	—
instUniformSpaceInt 📖	CompOp	2 math math: Int.isUniformEmbedding_coe_rat, Int.isUniformEmbedding_coe_real
instUniformSpaceMulOpposite 📖	CompOp	8 math math: CompleteSpace.mulOpposite, MulOpposite.uniformContinuousConstSMul, MulOpposite.instIsUniformGroup, MulOpposite.uniformContinuous_op, comap_uniformity_mulOpposite, DoubleCentralizer.isUniformEmbedding_toProdMulOpposite, MulOpposite.uniformContinuous_unop, uniformity_mulOpposite
instUniformSpaceMultiplicative 📖	CompOp	3 math math: uniformity_multiplicative, uniformContinuous_ofAdd, uniformContinuous_toAdd
instUniformSpaceNat 📖	CompOp	3 math math: Nat.isUniformEmbedding_coe_real, Nat.isUniformEmbedding_coe_rat, PNat.isUniformEmbedding_coe
instUniformSpacePUnit 📖	CompOp	2 math math: UniformEquiv.prodPUnit_apply, UniformEquiv.coe_punitProd
instUniformSpaceProd 📖	CompOp	84 math math: Bornology.IsBounded.uniformContinuousOn_smul, WithLp.toEquiv_uniformEquivProd, Filter.HasBasis.uniformity_prod, Prod.instIsUniformAddGroup, UniformContinuous.prodMap, uniformContinuous_mul, uniformContinuous₂_def, UniformCauchySeqOn.prod, UniformSpace.Completion.uniformContinuous_dist, IsUltraUniformity.prod, TendstoUniformly.prodMk, uniformContinuous₂_curry, Prod.instIsUniformGroup, IsUniformGroup.uniformContinuous_div, uniformContinuous_dist, IsUniformInducing.prod, instIsCountablyGeneratedProdUniformity, CauchySeq.prodMap, uniformContinuous_add, TendstoLocallyUniformlyOn.piProd, UniformCauchySeqOn.prod', DiscreteUniformity.instProd, IsUniformAddGroup.uniformContinuous_sub, UniformEquiv.prodCongr_symm, SeparationQuotient.uniformContinuous_dom₂, TopologicalSpace.NonemptyCompacts.uniformContinuous_sup, toTopologicalSpace_prod, Metric.uniformContinuous_infDist_Hausdorff_dist, uniformContinuous_vsub, uniformContinuous_nndist, TendstoUniformlyOnFilter.prodMk, UniformContinuous.prodMk, UniformEquiv.coe_prodComm, UniformEquiv.finTwoArrow_apply, Rat.uniformContinuous_add, uniformContinuous_swap, tendsto_prod_uniformity_snd, IsUniformEmbedding.prod, uniformity_prod_eq_prod, uniformContinuous_snd, TopologicalSpace.Compacts.uniformContinuous_sup, CompleteSpace.prod, cauchy_prod_iff, UniformEquiv.finTwoArrow_symm_apply, WithLp.prod_uniformContinuous_ofLp, Path.uniformContinuous_trans, tendsto_prod_uniformity_fst, TendstoUniformlyOnFilter.prodMap, SeparationQuotient.uniformContinuous_uncurry_lift₂, uniformContinuous_div, completeSpace_prod_of_nonempty, Cauchy.prod, UniformSpace.hausdorff.uniformContinuous_union, uniformContinuous_fst, TendstoLocallyUniformly.prodMk, UniformContinuous₂.uniformContinuous, TendstoUniformlyOn.prodMk, WithLp.isUniformInducing_toLp, CauchySeq.prodMk, entourageProd_mem_uniformity, UniformEquiv.prodPUnit_apply, uniformity_prod, Real.uniformContinuous_add, Unitization.isUniformEmbedding_addEquiv, UniformEquiv.coe_punitProd, TendstoUniformlyOn.prodMap, TendstoUniformly.prodMap, uniformity_prod_eq_comap_prod, TendstoLocallyUniformly.piProd, UniformEquiv.coe_prodCongr, TendstoLocallyUniformlyOn.prodMk, uniformContinuous_sub, TopologicalSpace.Closeds.uniformContinuous_sup, WithLp.toHomeomorph_uniformEquivProd, uniformContinuous_vadd, Unitization.uniformity_eq_aux, Real.uniformContinuous_mul, DoubleCentralizer.isUniformEmbedding_toProdMulOpposite, UniformEquiv.piFinTwo_symm_apply, Complex.isUniformEmbedding_equivRealProd, UniformCauchySeqOn.prodMap, UniformEquiv.piFinTwo_apply, UniformEquiv.prodComm_symm, WithLp.prod_uniformContinuous_toLp
instUniformSpaceSubtype 📖	CompOp	56 math math: Dynamics.coverEntropy_restrict, IsComplete.completeSpace_coe, ContinuousLinearMap.completeSpace_eqLocus, Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, MeasureTheory.Lp.simpleFunc.uniformContinuous, uniformity_setCoe, uniformEquicontinuous_restrict_iff, AddSubgroup.isUniformAddGroup, UniformContinuous.subtype_map, Subgroup.isUniformGroup, Algebra.elemental.instCompleteSpaceSubtypeMemSubalgebra, uniformContinuousOn_iff_restrict, Real.uniformContinuous_inv, Dynamics.coverEntropy_restrict_subset, isUniformInducing_rangeFactorization_iff, Path.uniformContinuous, UniformContinuous.rangeFactorization, isUniformEmbedding_set_inclusion, IsUniformInducing.rangeFactorization, LinearIsometryEquiv.completeSpace_map, isUniformEmbedding_subtypeEmb, MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace, NonUnitalAlgebra.elemental.instCompleteSpaceSubtypeMemNonUnitalSubalgebra, StarAlgebra.elemental.instCompleteSpaceSubtypeMemStarSubalgebra, Subtype.isComplete_iff, isUniformInducing_val, MeasureTheory.Lp.simpleFunc.isUniformEmbedding, LinearIsometry.completeSpace_map, instCompleteSpaceSubtypeMemSubmoduleOfIsClosedCoe, MeasureTheory.Lp.simpleFunc.isUniformInducing, uniformContinuous_rangeFactorization_iff, map_uniformity_set_coe, ContinuousLinearMap.completeSpace_ker, UniformEquiv.subtype_apply_coe, Valued.integer.totallyBounded_iff_finite_residueField, Submodule.instOrthogonalCompleteSpace, AntilipschitzWith.completeSpace_range_clm, ContinuousAlgHom.instCompleteSpaceSubtypeMemSubalgebraEqualizerOfT2SpaceOfContinuousMapClass, uniformity_subtype, IsClosed.completeSpace_coe, Real.uniformContinuous_mul, MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace, uniformContinuous_subtype_val, completeSpace_coe_iff_isComplete, IsNonarchimedeanLocalField.instCompleteSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation, instIsCountablyGeneratedProdElemUniformity, Subfield.completableTopField, NonUnitalStarAlgebra.elemental.instCompleteSpaceSubtypeMemNonUnitalStarSubalgebra, instCompleteSpaceSubtypeMemClosedSubmodule, UniformEquiv.subtype_symm_apply_coe, isUniformEmbedding_subtype_val, UniformContinuous.subtype_mk, toTopologicalSpace_subtype, Submodule.topologicalClosure.completeSpace, StarSubalgebra.instCompleteSpaceSubtypeMemTopologicalClosure, Dynamics.coverEntropyInf_restrict_subset
instUniqueUniformSpaceOfSubsingleton 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsSymm_entourageProd 📖	mathematical	—	SetRel.IsSymm entourageProd	—	SetRel.symm
ball_entourageProd 📖	mathematical	—	UniformSpace.ball entourageProd SProd.sprod Set Set.instSProd	—	Set.ext
ball_preimage 📖	mathematical	—	UniformSpace.ball Set.preimage	—	Set.ext
bot_uniformity 📖	mathematical	—	uniformity Bot.bot UniformSpace instBotUniformSpace Filter.principal SetRel.id	—	—
closure_ball_subset 📖	mathematical	—	Set Set.instHasSubset closure UniformSpace.toTopologicalSpace UniformSpace.ball instTopologicalSpaceProd	—	Continuous.closure_preimage_subset Continuous.prodMk_right
closure_eq_inter_uniformity 📖	mathematical	—	closure instTopologicalSpaceProd UniformSpace.toTopologicalSpace Set.iInter Set Filter Filter.instMembership uniformity SetRel.comp	—	closure_eq_uniformity Filter.HasBasis.biInter_mem UniformSpace.hasBasis_symmetric SetRel.comp_subset_comp SetRel.comp_subset_comp_left Set.iInter_congr_Prop SetRel.comp_assoc
closure_eq_uniformity 📖	mathematical	—	closure instTopologicalSpaceProd UniformSpace.toTopologicalSpace Set.iInter Set Set.instMembership setOf Filter Filter.instMembership uniformity SetRel.IsSymm SetRel.comp	—	Set.ext mem_closure_iff_nhds_basis UniformSpace.hasBasis_nhds_prod Set.inter_comm
comap_uniformity_addOpposite 📖	mathematical	—	Filter.comap AddOpposite AddOpposite.op uniformity instUniformSpaceAddOpposite	—	Filter.comap_comap Filter.comap_id
comap_uniformity_mulOpposite 📖	mathematical	—	Filter.comap MulOpposite MulOpposite.op uniformity instUniformSpaceMulOpposite	—	Filter.comap_comap Filter.comap_id
comp_open_symm_mem_uniformity_sets 📖	mathematical	SetRel Filter Filter.instMembership uniformity	Set IsOpen instTopologicalSpaceProd UniformSpace.toTopologicalSpace SetRel.IsSymm Set.instHasSubset SetRel.comp	—	comp_mem_uniformity_sets Filter.HasBasis.mem_iff uniformity_hasBasis_open_symmetric HasSubset.Subset.trans Set.instIsTransSubset SetRel.comp_subset_comp
discreteTopology_of_discrete_uniformity 📖	mathematical	uniformity Filter.principal SetRel.id	DiscreteTopology UniformSpace.toTopologicalSpace	—	UniformSpace.ext
entourageProd_mem_uniformity 📖	mathematical	SetRel Filter Filter.instMembership uniformity	instUniformSpaceProd entourageProd	—	uniformity_prod Filter.inter_mem_inf Filter.preimage_mem_comap
entourageProd_subset 📖	mathematical	Set Filter Filter.instMembership uniformity instUniformSpaceProd	SetRel Set.instHasSubset entourageProd	—	Filter.HasBasis.mem_iff' Filter.HasBasis.uniformity_prod Filter.basis_sets
eventually_uniformity_comp_subset 📖	mathematical	SetRel Filter Filter.instMembership uniformity	Filter.Eventually Set.instHasSubset SetRel.comp Filter.smallSets	—	eventually_uniformity_iterate_comp_subset
eventually_uniformity_iterate_comp_subset 📖	mathematical	SetRel Filter Filter.instMembership uniformity	Filter.Eventually Set.instHasSubset Nat.iterate SetRel.comp Filter.smallSets	—	comp_mem_uniformity_sets Filter.Eventually.mono Function.iterate_succ_apply' isRefl_of_mem_uniformity HasSubset.Subset.trans Set.instIsTransSubset SetRel.left_subset_comp SetRel.comp_subset_comp Filter.eventually_and
iInf_uniformity 📖	mathematical	—	uniformity iInf UniformSpace instInfSetUniformSpace Filter Filter.instInfSet	—	iInf_range
iSup_nhds_le_uniformity 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder iSup Filter.instSupSet nhds instTopologicalSpaceProd UniformSpace.toTopologicalSpace uniformity	—	iSup_le nhds_le_uniformity
image_entourageProd_prod 📖	mathematical	—	SetRel.image entourageProd SProd.sprod Set Set.instSProd	—	Set.ext
inf_uniformity 📖	mathematical	—	uniformity UniformSpace instMinUniformSpace Filter Filter.instInf	—	—
instIsCountablyGeneratedProdElemUniformity 📖	mathematical	—	Filter.IsCountablyGenerated Set.Elem uniformity instUniformSpaceSubtype Set Set.instMembership	—	Filter.comap.isCountablyGenerated
instIsCountablyGeneratedProdSumUniformity 📖	mathematical	—	Filter.IsCountablyGenerated uniformity Sum.instUniformSpace	—	Sum.uniformity Filter.Sup.isCountablyGenerated Filter.map.isCountablyGenerated
instIsCountablyGeneratedProdUniformity 📖	mathematical	—	Filter.IsCountablyGenerated uniformity instUniformSpaceProd	—	uniformity_prod Filter.Inf.isCountablyGenerated Filter.comap.isCountablyGenerated
interior_mem_uniformity 📖	mathematical	SetRel Filter Filter.instMembership uniformity	Set interior instTopologicalSpaceProd UniformSpace.toTopologicalSpace	—	uniformity_eq_uniformity_interior Filter.mem_lift'
inv_entourageProd 📖	mathematical	—	SetRel.inv entourageProd	—	—
isOpen_iff_isOpen_ball_subset 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace Set Filter Filter.instMembership uniformity instTopologicalSpaceProd Set.instHasSubset UniformSpace.ball	—	isOpen_iff_ball_subset interior_mem_uniformity isOpen_interior HasSubset.Subset.trans Set.instIsTransSubset UniformSpace.ball_mono interior_subset
le_iff_uniformContinuous_id 📖	mathematical	—	UniformSpace Preorder.toLE PartialOrder.toPreorder instPartialOrderUniformSpace UniformContinuous	—	uniformContinuous_iff uniformSpace_comap_id
map_uniformity_set_coe 📖	mathematical	—	Filter.map Set.Elem Set Set.instMembership uniformity instUniformSpaceSubtype Filter Filter.instInf Filter.principal SProd.sprod Set.instSProd	—	uniformity_setCoe Filter.map_comap Set.range_prodMap Subtype.range_val
mem_entourageProd 📖	mathematical	—	SetRel Set.instMembership entourageProd	—	—
mem_uniformity_isClosed 📖	mathematical	SetRel Filter Filter.instMembership uniformity	Set IsClosed instTopologicalSpaceProd UniformSpace.toTopologicalSpace Set.instHasSubset	—	Filter.HasBasis.mem_iff uniformity_hasBasis_closed
mem_uniformity_of_uniformContinuous_invariant 📖	mathematical	UniformContinuous instUniformSpaceProd SetRel Filter Filter.instMembership uniformity	Set Set.instMembership	—	Filter.mem_prod_iff Filter.mem_map Filter.tendsto_map'_iff uniformity_prod_eq_prod UniformContinuous.eq_1 refl_mem_uniformity
nhdsSet_diagonal_le_uniformity 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhdsSet instTopologicalSpaceProd UniformSpace.toTopologicalSpace Set.diagonal uniformity	—	Eq.trans_le nhdsSet_diagonal iSup_nhds_le_uniformity
nhds_eq_uniformity_prod 📖	mathematical	—	nhds instTopologicalSpaceProd UniformSpace.toTopologicalSpace Filter.lift' uniformity SProd.sprod Set Set.instSProd setOf SetRel Set.instMembership	—	nhds_prod_eq nhds_nhds_eq_uniformity_uniformity_prod Filter.lift_lift'_same_eq_lift' Monotone.set_prod monotone_const Set.monotone_preimage
nhds_le_uniformity 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds instTopologicalSpaceProd UniformSpace.toTopologicalSpace uniformity	—	comp_symm_mem_uniformity_sets nhds_prod_eq Filter.prod_mem_prod UniformSpace.ball_mem_nhds Filter.mem_of_superset UniformSpace.mem_comp_of_mem_ball
nhdset_of_mem_uniformity 📖	mathematical	SetRel Filter Filter.instMembership uniformity	IsOpen instTopologicalSpaceProd UniformSpace.toTopologicalSpace Set.instHasSubset setOf Set.instMembership	—	mem_nhds_iff nhds_eq_uniformity_prod Filter.mem_lift'_sets isOpen_iUnion Set.iUnion_subset
preimage_entourageProd_prod 📖	mathematical	—	SetRel.preimage entourageProd SProd.sprod Set Set.instSProd	—	image_entourageProd_prod
tendsto_of_uniformContinuous_subtype 📖	mathematical	UniformContinuous Set.Elem instUniformSpaceSubtype Set Set.instMembership Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace	Filter.Tendsto	—	mem_of_mem_nhds map_nhds_subtype_coe_eq_nhds Filter.tendsto_map' Continuous.continuousAt UniformContinuous.continuous
tendsto_prod_uniformity_fst 📖	mathematical	—	Filter.Tendsto uniformity instUniformSpaceProd	—	le_trans Filter.map_mono inf_le_left Filter.map_comap_le
tendsto_prod_uniformity_snd 📖	mathematical	—	Filter.Tendsto uniformity instUniformSpaceProd	—	le_trans Filter.map_mono inf_le_right Filter.map_comap_le
toTopologicalSpace_prod 📖	mathematical	—	UniformSpace.toTopologicalSpace instUniformSpaceProd instTopologicalSpaceProd	—	—
toTopologicalSpace_subtype 📖	mathematical	—	UniformSpace.toTopologicalSpace instUniformSpaceSubtype instTopologicalSpaceSubtype	—	—
top_uniformity 📖	mathematical	—	uniformity Top.top UniformSpace instTopUniformSpace Filter Filter.instTop	—	—
uniformContinuousOn_iff_restrict 📖	mathematical	—	UniformContinuousOn UniformContinuous Set.Elem instUniformSpaceSubtype Set Set.instMembership Set.restrict	—	map_uniformity_set_coe Filter.tendsto_map'_iff
uniformContinuous_comap 📖	mathematical	—	UniformContinuous UniformSpace.comap	—	Filter.tendsto_comap
uniformContinuous_comap' 📖	mathematical	UniformContinuous	UniformSpace.comap	—	Filter.tendsto_comap_iff
uniformContinuous_fst 📖	mathematical	—	UniformContinuous instUniformSpaceProd	—	tendsto_prod_uniformity_fst
uniformContinuous_iInf_dom 📖	mathematical	UniformContinuous	iInf UniformSpace instInfSetUniformSpace	—	iInf_uniformity Filter.tendsto_iInf'
uniformContinuous_iInf_rng 📖	mathematical	—	UniformContinuous iInf UniformSpace instInfSetUniformSpace	—	iInf_uniformity Filter.tendsto_iInf
uniformContinuous_iff 📖	mathematical	—	UniformContinuous UniformSpace Preorder.toLE PartialOrder.toPreorder instPartialOrderUniformSpace UniformSpace.comap	—	Filter.map_le_iff_le_comap
uniformContinuous_inf_dom_left₂ 📖	mathematical	UniformContinuous instUniformSpaceProd	UniformSpace instMinUniformSpace	—	UniformContinuous.inf_dom_left uniformContinuous_id UniformContinuous.prodMap UniformContinuous.comp
uniformContinuous_inf_dom_right₂ 📖	mathematical	UniformContinuous instUniformSpaceProd	UniformSpace instMinUniformSpace	—	UniformContinuous.inf_dom_right uniformContinuous_id UniformContinuous.prodMap UniformContinuous.comp
uniformContinuous_inl 📖	mathematical	—	UniformContinuous Sum.instUniformSpace	—	le_sup_left
uniformContinuous_inr 📖	mathematical	—	UniformContinuous Sum.instUniformSpace	—	le_sup_right
uniformContinuous_ofAdd 📖	mathematical	—	UniformContinuous Multiplicative instUniformSpaceMultiplicative DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	uniformContinuous_id
uniformContinuous_ofMul 📖	mathematical	—	UniformContinuous Additive instUniformSpaceAdditive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	uniformContinuous_id
uniformContinuous_sInf_dom 📖	mathematical	UniformSpace Set Set.instMembership UniformContinuous	InfSet.sInf instInfSetUniformSpace	—	sInf_eq_iInf' iInf_uniformity Filter.tendsto_iInf'
uniformContinuous_sInf_dom₂ 📖	mathematical	UniformSpace Set Set.instMembership UniformContinuous instUniformSpaceProd	InfSet.sInf instInfSetUniformSpace	—	uniformContinuous_sInf_dom uniformContinuous_id UniformContinuous.prodMap UniformContinuous.comp
uniformContinuous_sInf_rng 📖	mathematical	—	UniformContinuous InfSet.sInf UniformSpace instInfSetUniformSpace	—	sInf_eq_iInf' iInf_uniformity Filter.tendsto_iInf SetCoe.forall
uniformContinuous_snd 📖	mathematical	—	UniformContinuous instUniformSpaceProd	—	tendsto_prod_uniformity_snd
uniformContinuous_subtype_val 📖	mathematical	—	UniformContinuous instUniformSpaceSubtype	—	uniformContinuous_comap
uniformContinuous_swap 📖	mathematical	—	UniformContinuous instUniformSpaceProd	—	UniformContinuous.prodMk uniformContinuous_snd uniformContinuous_fst
uniformContinuous_toAdd 📖	mathematical	—	UniformContinuous Multiplicative instUniformSpaceMultiplicative DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd	—	uniformContinuous_id
uniformContinuous_toMul 📖	mathematical	—	UniformContinuous Additive instUniformSpaceAdditive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.toMul	—	uniformContinuous_id
uniformContinuous₂_curry 📖	mathematical	—	UniformContinuous₂ UniformContinuous instUniformSpaceProd	—	UniformContinuous₂.eq_1
uniformContinuous₂_def 📖	mathematical	—	UniformContinuous₂ UniformContinuous instUniformSpaceProd	—	—
uniformSpace_comap_id 📖	mathematical	—	UniformSpace.comap UniformSpace	—	UniformSpace.ext uniformity_comap Filter.comap_id
uniformity_addOpposite 📖	mathematical	—	uniformity AddOpposite instUniformSpaceAddOpposite Filter.comap AddOpposite.unop	—	—
uniformity_additive 📖	mathematical	—	uniformity Additive instUniformSpaceAdditive Filter.map DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	—
uniformity_comap 📖	mathematical	—	uniformity UniformSpace.comap Filter.comap	—	—
uniformity_eq_uniformity_closure 📖	mathematical	—	uniformity Filter.lift' closure instTopologicalSpaceProd UniformSpace.toTopologicalSpace	—	Filter.HasBasis.lift'_closure_eq_self uniformity_hasBasis_closed
uniformity_eq_uniformity_interior 📖	mathematical	—	uniformity Filter.lift' interior instTopologicalSpaceProd UniformSpace.toTopologicalSpace	—	le_antisymm le_iInf₂ comp3_mem_uniformity nhdset_of_mem_uniformity IsOpen.subset_interior_iff Filter.mp_mem Filter.univ_mem' Filter.sets_of_superset Filter.mem_lift' interior_subset
uniformity_hasBasis_closed 📖	mathematical	—	Filter.HasBasis SetRel uniformity Filter Filter.instMembership IsClosed instTopologicalSpaceProd UniformSpace.toTopologicalSpace	—	Filter.hasBasis_self comp_comp_symm_mem_uniformity_sets Filter.mem_of_superset subset_closure isClosed_closure Set.Subset.trans closure_eq_uniformity Set.iInter_subset_of_subset Set.iInter_subset
uniformity_hasBasis_closure 📖	mathematical	—	Filter.HasBasis SetRel uniformity Filter Filter.instMembership closure instTopologicalSpaceProd UniformSpace.toTopologicalSpace	—	Filter.HasBasis.uniformity_closure Filter.basis_sets
uniformity_hasBasis_open 📖	mathematical	—	Filter.HasBasis SetRel uniformity Filter Filter.instMembership IsOpen instTopologicalSpaceProd UniformSpace.toTopologicalSpace	—	Filter.hasBasis_self interior_mem_uniformity isOpen_interior interior_subset
uniformity_hasBasis_open_symmetric 📖	mathematical	—	Filter.HasBasis SetRel uniformity Filter Filter.instMembership IsOpen instTopologicalSpaceProd UniformSpace.toTopologicalSpace SetRel.IsSymm	—	Filter.HasBasis.restrict uniformity_hasBasis_open symmetrize_mem_uniformity IsOpen.inter IsOpen.preimage continuous_swap SetRel.isSymm_symmetrize SetRel.symmetrize_subset_self
uniformity_mulOpposite 📖	mathematical	—	uniformity MulOpposite instUniformSpaceMulOpposite Filter.comap MulOpposite.unop	—	—
uniformity_multiplicative 📖	mathematical	—	uniformity Multiplicative instUniformSpaceMultiplicative Filter.map DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	—
uniformity_prod 📖	mathematical	—	uniformity instUniformSpaceProd Filter Filter.instInf Filter.comap	—	—
uniformity_prod_eq_comap_prod 📖	mathematical	—	uniformity instUniformSpaceProd Filter.comap SProd.sprod Filter Filter.instSProd	—	Filter.comap_inf Filter.comap_comap
uniformity_prod_eq_prod 📖	mathematical	—	uniformity instUniformSpaceProd Filter.map SProd.sprod Filter Filter.instSProd	—	Filter.map_swap4_eq_comap uniformity_prod_eq_comap_prod
uniformity_setCoe 📖	mathematical	—	uniformity Set.Elem instUniformSpaceSubtype Set Set.instMembership Filter.comap	—	—
uniformity_subtype 📖	mathematical	—	uniformity instUniformSpaceSubtype Filter.comap	—	—
union_mem_uniformity_sum 📖	mathematical	SetRel Filter Filter.instMembership uniformity	Set Sum.instUniformSpace Set.instUnion Set.image	—	Filter.union_mem_sup Filter.image_mem_map

---

← Back to Index