Closeds

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

Statistics

Metric	Count
Definitions Closeds, Closeds, uniformSpace, uniformSpace, uniformSpace, hausdorff, hausdorffEntourage	7
Theorems uniformity_closeds, uniformity_compacts, uniformity_hausdorff, uniformity_nonemptyCompacts, powerset_hausdorff, nhds_hausdorff_eq_nhds_vietoris, compacts_map, image_hausdorff, nonemptyCompacts_map, compacts_map, image_hausdorff, nonemptyCompacts_map, compactSpace_iff, continuous_closure, continuous_singleton, discreteUniformity_iff, instCompactSpace, instContinuousSup, instDiscreteUniformity, instNoncompactSpace, instT0Space, isClopen_singleton_bot, isClosedEmbedding_singleton, isClosed_subsets_of_isClosed, isEmbedding_singleton, isOpen_inter_nonempty_of_isOpen, isUniformEmbedding_coe, isUniformEmbedding_singleton, isUniformInducing_closure, noncompactSpace_iff, totallyBounded_subsets_of_totallyBounded, uniformContinuous_closure, uniformContinuous_coe, uniformContinuous_singleton, uniformContinuous_sup, uniformity_def, continuous_toCloseds, discreteUniformity_iff, instDiscreteUniformity, isEmbedding_toCloseds, isUniformEmbedding_coe, isUniformEmbedding_singleton, isUniformEmbedding_toCloseds, totallyBounded_subsets_of_totallyBounded, uniformContinuous_coe, uniformContinuous_singleton, uniformContinuous_sup, uniformContinuous_toCloseds, uniformity_def, continuous_toCloseds, discreteUniformity_iff, instDiscreteUniformity, isEmbedding_toCloseds, isUniformEmbedding_coe, isUniformEmbedding_singleton, isUniformEmbedding_toCloseds, isUniformEmbedding_toCompacts, totallyBounded_subsets_of_totallyBounded, uniformContinuous_coe, uniformContinuous_singleton, uniformContinuous_sup, uniformContinuous_toCloseds, uniformContinuous_toCompacts, uniformity_def, exists_prodMk_finset_mem_hausdorffEntourage, nhds_vietoris_le_nhds_hausdorff, powerset_hausdorff, compacts_map, image_hausdorff, nonemptyCompacts_map, sup_closeds, sup_compacts, sup_nonemptyCompacts, continuous_closure, instCompactSpaceSet, instDiscreteUniformitySet, isClopen_singleton_empty, isClosedEmbedding_singleton, isClosed_powerset, isOpen_inter_nonempty_of_isOpen, isUniformEmbedding_singleton, isUniformInducing_closure, nhds_closure, uniformContinuous_closure, uniformContinuous_union, hausdorffEntourage_comp, hausdorffEntourage_id, hausdorffEntourage_mono, inv_hausdorffEntourage, isRefl_hausdorffEntourage, isSymm_hausdorffEntourage, isTrans_hausdorffEntourage, mem_hausdorffEntourage, monotone_hausdorffEntourage, singleton_mem_hausdorffEntourage, union_mem_hausdorffEntourage	96
Total	103

ClosureOperator

Definitions

Name	Category	Theorems
Closeds 📖	CompOp	1 math math: closureOperator_gi_self

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformity_closeds 📖	mathematical	Filter.HasBasis uniformity	TopologicalSpace.Closeds UniformSpace.toTopologicalSpace TopologicalSpace.Closeds.uniformSpace Set.preimage Set SetLike.coe TopologicalSpace.Closeds.instSetLike hausdorffEntourage	—	comap uniformity_hausdorff
uniformity_compacts 📖	mathematical	Filter.HasBasis uniformity	TopologicalSpace.Compacts UniformSpace.toTopologicalSpace TopologicalSpace.Compacts.uniformSpace Set.preimage Set SetLike.coe TopologicalSpace.Compacts.instSetLike hausdorffEntourage	—	comap uniformity_hausdorff
uniformity_hausdorff 📖	mathematical	Filter.HasBasis uniformity	Set UniformSpace.hausdorff SetRel hausdorffEntourage	—	lift' monotone_hausdorffEntourage
uniformity_nonemptyCompacts 📖	mathematical	Filter.HasBasis uniformity	TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace TopologicalSpace.NonemptyCompacts.uniformSpace Set.preimage Set SetLike.coe TopologicalSpace.NonemptyCompacts.instSetLike hausdorffEntourage	—	comap uniformity_hausdorff

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
powerset_hausdorff 📖	mathematical	—	IsClosed Set UniformSpace.toTopologicalSpace UniformSpace.hausdorff Set.powerset	—	UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen isOpen_compl

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nhds_hausdorff_eq_nhds_vietoris 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace	nhds Set UniformSpace.hausdorff TopologicalSpace.vietoris	—	le_antisymm TopologicalSpace.nhds_generateFrom Filter.HasBasis.mem_iff nhdsSet_basis_uniformity Filter.basis_sets IsOpen.mem_nhdsSet Filter.mp_mem UniformSpace.ball_mem_nhds Filter.mem_lift' Filter.univ_mem' HasSubset.Subset.trans Set.instIsTransSubset Set.mem_biUnion IsOpen.mem_nhds UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen TotallyBounded.nhds_vietoris_le_nhds_hausdorff totallyBounded

IsUniformEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compacts_map 📖	mathematical	IsUniformEmbedding	TopologicalSpace.Compacts UniformSpace.toTopologicalSpace TopologicalSpace.Compacts.uniformSpace TopologicalSpace.Compacts.map UniformContinuous.continuous IsUniformInducing.uniformContinuous toIsUniformInducing	—	UniformContinuous.continuous IsUniformInducing.uniformContinuous isUniformInducing IsUniformInducing.compacts_map toIsUniformInducing TopologicalSpace.Compacts.map_injective injective
image_hausdorff 📖	mathematical	IsUniformEmbedding	Set UniformSpace.hausdorff Set.image	—	IsUniformInducing.image_hausdorff isUniformInducing Function.Injective.image_injective injective
nonemptyCompacts_map 📖	mathematical	IsUniformEmbedding	TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace TopologicalSpace.NonemptyCompacts.uniformSpace TopologicalSpace.NonemptyCompacts.map UniformContinuous.continuous IsUniformInducing.uniformContinuous toIsUniformInducing	—	UniformContinuous.continuous IsUniformInducing.uniformContinuous isUniformInducing IsUniformInducing.nonemptyCompacts_map toIsUniformInducing TopologicalSpace.NonemptyCompacts.map_injective injective

IsUniformInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compacts_map 📖	mathematical	IsUniformInducing	TopologicalSpace.Compacts UniformSpace.toTopologicalSpace TopologicalSpace.Compacts.uniformSpace TopologicalSpace.Compacts.map UniformContinuous.continuous uniformContinuous	—	of_comp UniformContinuous.continuous uniformContinuous UniformContinuous.compacts_map TopologicalSpace.Compacts.uniformContinuous_coe comp image_hausdorff IsUniformEmbedding.isUniformInducing TopologicalSpace.Compacts.isUniformEmbedding_coe
image_hausdorff 📖	mathematical	IsUniformInducing	Set UniformSpace.hausdorff Set.image	—	Filter.comap_lift'_eq comap_uniformity Filter.comap_lift'_eq2 monotone_hausdorffEntourage Set.ext
nonemptyCompacts_map 📖	mathematical	IsUniformInducing	TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace TopologicalSpace.NonemptyCompacts.uniformSpace TopologicalSpace.NonemptyCompacts.map UniformContinuous.continuous uniformContinuous	—	of_comp UniformContinuous.continuous uniformContinuous UniformContinuous.nonemptyCompacts_map TopologicalSpace.NonemptyCompacts.uniformContinuous_coe comp image_hausdorff IsUniformEmbedding.isUniformInducing TopologicalSpace.NonemptyCompacts.isUniformEmbedding_coe

TopologicalSpace

Definitions

Name	Category	Theorems
Closeds 📖	CompData	145 math math: NonemptyCompacts.uniformContinuous_toCloseds, Closeds.uniformContinuous_closure, Compacts.toCloseds_singleton, Closeds.iInf_def, AlgebraicGeometry.Scheme.support_nilradical, ClosedSubmodule.toCloseds_injective, Closeds.coe_compl, NonemptyCompacts.toCloseds_injective, Closeds.complOrderIso_symm_apply, Closeds.noncompactSpace_iff, Closeds.isClosed, AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp, Closeds.mem_singleton, AlgebraicGeometry.Scheme.IdealSheafData.gc, EMetric.NonemptyCompacts.isometry_toCloseds, EMetric.NonemptyCompacts.isUniformEmbedding_toCloseds, Compacts.coe_toCloseds, Closeds.isUniformEmbedding_coe, Opens.isCoatom_iff, EMetric.Closeds.isometry_singleton, NonemptyCompacts.isClosed_in_closeds, AlgebraicGeometry.Scheme.IdealSheafData.support_mul, Closeds.coe_iInf, Closeds.ext_iff, Opens.complOrderIso_apply, Closeds.instContinuousSup, Closeds.closure_le, Closeds.coe_eq_empty, Opens.complOrderIso_symm_apply, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_mkOfMemSupportIff, NoetherianSpace.exists_finset_irreducible, Closeds.coe_preimage, Closeds.singleton_inj, Closeds.gc, Closeds.continuous_closure, Filter.HasBasis.uniformity_closeds, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, Closeds.mk_singleton, Closeds.singleton_injective, Closeds.uniformity_def, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem, NonemptyCompacts.mem_toCloseds, NonemptyCompacts.coe_toCloseds, Closeds.instNoncompactSpace, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, Closeds.mem_sInf, Closeds.complOrderIso_apply, Closeds.coe_singleton, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff, AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal, NonemptyCompacts.isEmbedding_toCloseds, Compacts.uniformContinuous_toCloseds, Closeds.lipschitz_sup, Opens.compl_bijective, EMetric.isClosed_subsets_of_isClosed, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, AlgebraicGeometry.Scheme.IdealSheafData.support_antitone, Closeds.coe_bot, Compacts.isUniformEmbedding_toCloseds, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff, Closeds.edist_eq, Closeds.isometry_singleton, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_mem_support, Compacts.toCloseds_injective, Closeds.coe_finset_inf, ClosedSubmodule.coe_toCloseds, Compacts.mem_toCloseds, Closeds.isClosed_subsets_of_isClosed, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sup, Closeds.instCompactSpace, Closeds.coe_nonempty, NonemptyCompacts.isUniformEmbedding_toCloseds, Closeds.instDiscreteUniformity, Closeds.continuous_infEDist, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_bot_iff, Closeds.isAtom_iff, AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal, NonemptyCompacts.isometry_toCloseds, noetherianSpace_TFAE, AlgebraicGeometry.Scheme.IdealSheafData.support_iSup, Closeds.instCompleteSpace, Closeds.continuous_singleton, Closeds.coe_inf, Closeds.carrier_eq_coe, Closeds.coe_sup, Closeds.coe_top, EMetric.NonemptyCompacts.isClosed_in_closeds, PrimitiveSpectrum.closedsGC_closureOperator, Closeds.coe_finset_sup, Closeds.coe_eq_univ, NoetherianSpace.exists_finite_set_closeds_irreducible, instWellFoundedLTClosedsOfNoetherianSpace, Closeds.coe_mk, Closeds.coe_sSup, Compacts.continuous_toCloseds, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, Opens.coe_compl, Closeds.isClopen_singleton_bot, Closeds.iInf_mk, AlgebraicGeometry.Scheme.IdealSheafData.support_map, Clopens.coe_toCloseds, Closeds.isAtom_coe, Closeds.mem_closure, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top, Closeds.totallyBounded_subsets_of_totallyBounded, NonemptyCompacts.continuous_toCloseds, AlgebraicGeometry.Scheme.Hom.range_subset_ker_support, EMetric.NonemptyCompacts.ToCloseds.isUniformEmbedding, Closeds.compl_bijective, EMetric.Closeds.lipschitz_sup, Closeds.isUniformEmbedding_singleton, Closeds.compactSpace_iff, Closeds.uniformContinuous_sup, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, AlgebraicGeometry.Scheme.Hom.support_ker, Compacts.isEmbedding_toCloseds, AlgebraicGeometry.Scheme.IdealSheafData.support_top, Closeds.coe_closure, Closeds.uniformContinuous_coe, Closeds.isUniformInducing_closure, EMetric.NonemptyCompacts.continuous_toCloseds, Closeds.isClosedEmbedding_singleton, Closeds.mem_mk, EMetric.Closeds.edist_eq, Closeds.coe_sInf, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_vanishingIdeal, EMetric.Closeds.isClosed_subsets_of_isClosed, AlgebraicGeometry.Scheme.IdealSheafData.support_bot, NonemptyCompacts.toCloseds_singleton, AlgebraicGeometry.Scheme.IdealSheafData.support_sup, Closeds.mem_iInf, AlgebraicGeometry.Scheme.IdealSheafData.support_sSup, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup, Compacts.isometry_toCloseds, Closeds.isEmbedding_singleton, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sSup, Closeds.uniformContinuous_singleton, Closeds.instCanLiftSetCoeIsClosed, Closeds.discreteUniformity_iff, EMetric.continuous_infEdist_hausdorffEdist, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_bot, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply, Closeds.instT0Space, Closeds.isOpen_inter_nonempty_of_isOpen

TopologicalSpace.Closeds

Definitions

Name	Category	Theorems
uniformSpace 📖	CompOp	43 math math: TopologicalSpace.NonemptyCompacts.uniformContinuous_toCloseds, uniformContinuous_closure, noncompactSpace_iff, EMetric.NonemptyCompacts.isUniformEmbedding_toCloseds, isUniformEmbedding_coe, TopologicalSpace.NonemptyCompacts.isClosed_in_closeds, instContinuousSup, continuous_closure, Filter.HasBasis.uniformity_closeds, uniformity_def, instNoncompactSpace, TopologicalSpace.NonemptyCompacts.isEmbedding_toCloseds, TopologicalSpace.Compacts.uniformContinuous_toCloseds, EMetric.isClosed_subsets_of_isClosed, TopologicalSpace.Compacts.isUniformEmbedding_toCloseds, isClosed_subsets_of_isClosed, instCompactSpace, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds, instDiscreteUniformity, continuous_infEDist, instCompleteSpace, continuous_singleton, EMetric.NonemptyCompacts.isClosed_in_closeds, TopologicalSpace.Compacts.continuous_toCloseds, isClopen_singleton_bot, totallyBounded_subsets_of_totallyBounded, TopologicalSpace.NonemptyCompacts.continuous_toCloseds, EMetric.NonemptyCompacts.ToCloseds.isUniformEmbedding, isUniformEmbedding_singleton, compactSpace_iff, uniformContinuous_sup, TopologicalSpace.Compacts.isEmbedding_toCloseds, uniformContinuous_coe, isUniformInducing_closure, EMetric.NonemptyCompacts.continuous_toCloseds, isClosedEmbedding_singleton, EMetric.Closeds.isClosed_subsets_of_isClosed, isEmbedding_singleton, uniformContinuous_singleton, discreteUniformity_iff, EMetric.continuous_infEdist_hausdorffEdist, instT0Space, isOpen_inter_nonempty_of_isOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace_iff 📖	mathematical	—	CompactSpace TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace	—	compactSpace_of_finite_subfamily_closed IsCompact.elim_finite_subfamily_closed IsClosed.isCompact IsClopen.isClosed IsClopen.compl isClopen_singleton_bot isClosed_subsets_of_isClosed Set.iInter_congr_Prop Set.Subset.rfl isClosed_biInter instCompactSpace
continuous_closure 📖	mathematical	—	Continuous Set TopologicalSpace.Closeds UniformSpace.toTopologicalSpace UniformSpace.hausdorff uniformSpace closure	—	UniformContinuous.continuous uniformContinuous_closure
continuous_singleton 📖	mathematical	—	Continuous TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace instSingletonOfT1Space T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace	—	Topology.IsEmbedding.continuous T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace isEmbedding_singleton
discreteUniformity_iff 📖	mathematical	—	DiscreteUniformity TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace	—	IsUniformEmbedding.discreteUniformity T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace isUniformEmbedding_singleton instDiscreteUniformity
instCompactSpace 📖	mathematical	—	CompactSpace TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace	—	Set.image_univ Function.Surjective.range_eq GaloisInsertion.l_surjective IsCompact.image isCompact_univ UniformSpace.hausdorff.instCompactSpaceSet continuous_closure
instContinuousSup 📖	mathematical	—	ContinuousSup TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	UniformContinuous.continuous uniformContinuous_sup
instDiscreteUniformity 📖	mathematical	—	DiscreteUniformity TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace	—	IsUniformEmbedding.discreteUniformity UniformSpace.hausdorff.instDiscreteUniformitySet isUniformEmbedding_coe
instNoncompactSpace 📖	mathematical	—	NoncompactSpace TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace	—	noncompactSpace_iff
instT0Space 📖	mathematical	—	T0Space TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace	—	isClosed_iff_frequently isClosed nhds_eq_comap_uniformity Filter.frequently_comap Filter.frequently_iff mem_of_mem_nhds Inseparable.nhds_le_uniformity Filter.preimage_mem_comap Filter.mem_lift' le_antisymm Inseparable.symm
isClopen_singleton_bot 📖	mathematical	—	IsClopen TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace Set Set.instSingletonSet Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Set.ext IsClopen.preimage UniformSpace.hausdorff.isClopen_singleton_empty UniformContinuous.continuous uniformContinuous_coe
isClosedEmbedding_singleton 📖	mathematical	—	Topology.IsClosedEmbedding TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace instSingletonOfT1Space T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace	—	T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace IsUniformEmbedding.isEmbedding isUniformEmbedding_singleton Function.Injective.preimage_image SetLike.coe_injective Set.range_comp IsClosed.preimage UniformContinuous.continuous uniformContinuous_coe Topology.IsClosedEmbedding.isClosed_range UniformSpace.hausdorff.isClosedEmbedding_singleton
isClosed_subsets_of_isClosed 📖	mathematical	—	IsClosed TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace setOf Set Set.instHasSubset SetLike.coe instSetLike	—	isClosed_induced IsClosed.powerset_hausdorff
isEmbedding_singleton 📖	mathematical	—	Topology.IsEmbedding TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace instSingletonOfT1Space T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace	—	IsUniformEmbedding.isEmbedding T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace isUniformEmbedding_singleton
isOpen_inter_nonempty_of_isOpen 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace	TopologicalSpace.Closeds uniformSpace setOf Set.Nonempty Set Set.instInter SetLike.coe instSetLike	—	isOpen_induced UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen
isUniformEmbedding_coe 📖	mathematical	—	IsUniformEmbedding TopologicalSpace.Closeds UniformSpace.toTopologicalSpace Set uniformSpace UniformSpace.hausdorff SetLike.coe instSetLike	—	SetLike.coe_injective
isUniformEmbedding_singleton 📖	mathematical	—	IsUniformEmbedding TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace instSingletonOfT1Space T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace	—	T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace IsUniformEmbedding.of_comp_iff isUniformEmbedding_coe UniformSpace.hausdorff.isUniformEmbedding_singleton
isUniformInducing_closure 📖	mathematical	—	IsUniformInducing Set TopologicalSpace.Closeds UniformSpace.toTopologicalSpace UniformSpace.hausdorff uniformSpace closure	—	IsUniformInducing.isUniformInducing_comp_iff IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_coe UniformSpace.hausdorff.isUniformInducing_closure
noncompactSpace_iff 📖	mathematical	—	NoncompactSpace TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace	—	—
totallyBounded_subsets_of_totallyBounded 📖	mathematical	TotallyBounded	TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace setOf Set Set.instHasSubset SetLike.coe instSetLike	—	totallyBounded_preimage IsUniformEmbedding.isUniformInducing isUniformEmbedding_coe TotallyBounded.powerset_hausdorff
uniformContinuous_closure 📖	mathematical	—	UniformContinuous Set TopologicalSpace.Closeds UniformSpace.toTopologicalSpace UniformSpace.hausdorff uniformSpace closure	—	IsUniformInducing.uniformContinuous isUniformInducing_closure
uniformContinuous_coe 📖	mathematical	—	UniformContinuous TopologicalSpace.Closeds UniformSpace.toTopologicalSpace Set uniformSpace UniformSpace.hausdorff SetLike.coe instSetLike	—	IsUniformInducing.uniformContinuous IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_coe
uniformContinuous_singleton 📖	mathematical	—	UniformContinuous TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace instSingletonOfT1Space T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace	—	IsUniformInducing.uniformContinuous T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_singleton
uniformContinuous_sup 📖	mathematical	—	UniformContinuous TopologicalSpace.Closeds UniformSpace.toTopologicalSpace instUniformSpaceProd uniformSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	IsUniformInducing.uniformContinuous_iff IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_coe UniformContinuous.comp UniformSpace.hausdorff.uniformContinuous_union UniformContinuous.prodMap uniformContinuous_coe
uniformity_def 📖	mathematical	—	uniformity TopologicalSpace.Closeds UniformSpace.toTopologicalSpace uniformSpace Filter.comap Set SetLike.coe instSetLike Filter.lift' hausdorffEntourage	—	—

TopologicalSpace.Compacts

Definitions

Name	Category	Theorems
uniformSpace 📖	CompOp	17 math math: uniformContinuous_singleton, uniformity_def, totallyBounded_subsets_of_totallyBounded, Filter.HasBasis.uniformity_compacts, discreteUniformity_iff, uniformContinuous_toCloseds, IsUniformInducing.compacts_map, isUniformEmbedding_toCloseds, IsUniformEmbedding.compacts_map, uniformContinuous_sup, UniformContinuous.compacts_map, isUniformEmbedding_singleton, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCompacts, uniformContinuous_coe, instDiscreteUniformity, isUniformEmbedding_coe, TopologicalSpace.NonemptyCompacts.uniformContinuous_toCompacts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_toCloseds 📖	mathematical	—	Continuous TopologicalSpace.Compacts UniformSpace.toTopologicalSpace TopologicalSpace.Closeds topology TopologicalSpace.Closeds.uniformSpace toCloseds	—	UniformContinuous.continuous uniformContinuous_toCloseds
discreteUniformity_iff 📖	mathematical	—	DiscreteUniformity TopologicalSpace.Compacts UniformSpace.toTopologicalSpace uniformSpace	—	IsUniformEmbedding.discreteUniformity isUniformEmbedding_singleton instDiscreteUniformity
instDiscreteUniformity 📖	mathematical	—	DiscreteUniformity TopologicalSpace.Compacts UniformSpace.toTopologicalSpace uniformSpace	—	IsUniformEmbedding.discreteUniformity UniformSpace.hausdorff.instDiscreteUniformitySet isUniformEmbedding_coe
isEmbedding_toCloseds 📖	mathematical	—	Topology.IsEmbedding TopologicalSpace.Compacts UniformSpace.toTopologicalSpace TopologicalSpace.Closeds topology TopologicalSpace.Closeds.uniformSpace toCloseds	—	IsUniformEmbedding.isEmbedding isUniformEmbedding_toCloseds
isUniformEmbedding_coe 📖	mathematical	—	IsUniformEmbedding TopologicalSpace.Compacts UniformSpace.toTopologicalSpace Set uniformSpace UniformSpace.hausdorff SetLike.coe instSetLike	—	SetLike.coe_injective
isUniformEmbedding_singleton 📖	mathematical	—	IsUniformEmbedding TopologicalSpace.Compacts UniformSpace.toTopologicalSpace uniformSpace instSingleton	—	IsUniformEmbedding.of_comp_iff isUniformEmbedding_coe UniformSpace.hausdorff.isUniformEmbedding_singleton
isUniformEmbedding_toCloseds 📖	mathematical	—	IsUniformEmbedding TopologicalSpace.Compacts UniformSpace.toTopologicalSpace TopologicalSpace.Closeds uniformSpace TopologicalSpace.Closeds.uniformSpace toCloseds	—	Filter.comap_comap toCloseds_injective
totallyBounded_subsets_of_totallyBounded 📖	mathematical	TotallyBounded	TopologicalSpace.Compacts UniformSpace.toTopologicalSpace uniformSpace setOf Set Set.instHasSubset SetLike.coe instSetLike	—	totallyBounded_preimage IsUniformEmbedding.isUniformInducing isUniformEmbedding_coe TotallyBounded.powerset_hausdorff
uniformContinuous_coe 📖	mathematical	—	UniformContinuous TopologicalSpace.Compacts UniformSpace.toTopologicalSpace Set uniformSpace UniformSpace.hausdorff SetLike.coe instSetLike	—	IsUniformInducing.uniformContinuous IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_coe
uniformContinuous_singleton 📖	mathematical	—	UniformContinuous TopologicalSpace.Compacts UniformSpace.toTopologicalSpace uniformSpace instSingleton	—	IsUniformInducing.uniformContinuous IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_singleton
uniformContinuous_sup 📖	mathematical	—	UniformContinuous TopologicalSpace.Compacts UniformSpace.toTopologicalSpace instUniformSpaceProd uniformSpace instMax	—	IsUniformInducing.uniformContinuous_iff IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_coe UniformContinuous.comp UniformSpace.hausdorff.uniformContinuous_union UniformContinuous.prodMap uniformContinuous_coe
uniformContinuous_toCloseds 📖	mathematical	—	UniformContinuous TopologicalSpace.Compacts UniformSpace.toTopologicalSpace TopologicalSpace.Closeds uniformSpace TopologicalSpace.Closeds.uniformSpace toCloseds	—	IsUniformInducing.uniformContinuous IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_toCloseds
uniformity_def 📖	mathematical	—	uniformity TopologicalSpace.Compacts UniformSpace.toTopologicalSpace uniformSpace Filter.comap Set SetLike.coe instSetLike Filter.lift' hausdorffEntourage	—	—

TopologicalSpace.NonemptyCompacts

Definitions

Name	Category	Theorems
uniformSpace 📖	CompOp	21 math math: uniformContinuous_toCloseds, EMetric.NonemptyCompacts.isUniformEmbedding_toCloseds, Filter.HasBasis.uniformity_nonemptyCompacts, uniformContinuous_coe, uniformity_def, uniformContinuous_singleton, instDiscreteUniformity, uniformContinuous_sup, Metric.uniformContinuous_infDist_Hausdorff_dist, isUniformEmbedding_coe, isUniformEmbedding_toCloseds, totallyBounded_subsets_of_totallyBounded, isUniformEmbedding_toCompacts, isUniformEmbedding_singleton, instCompleteSpace, discreteUniformity_iff, UniformContinuous.nonemptyCompacts_map, EMetric.NonemptyCompacts.ToCloseds.isUniformEmbedding, uniformContinuous_toCompacts, IsUniformInducing.nonemptyCompacts_map, IsUniformEmbedding.nonemptyCompacts_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_toCloseds 📖	mathematical	—	Continuous TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace TopologicalSpace.Closeds topology TopologicalSpace.Closeds.uniformSpace toCloseds	—	UniformContinuous.continuous uniformContinuous_toCloseds
discreteUniformity_iff 📖	mathematical	—	DiscreteUniformity TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace uniformSpace	—	IsUniformEmbedding.discreteUniformity isUniformEmbedding_singleton instDiscreteUniformity
instDiscreteUniformity 📖	mathematical	—	DiscreteUniformity TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace uniformSpace	—	IsUniformEmbedding.discreteUniformity UniformSpace.hausdorff.instDiscreteUniformitySet isUniformEmbedding_coe
isEmbedding_toCloseds 📖	mathematical	—	Topology.IsEmbedding TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace TopologicalSpace.Closeds topology TopologicalSpace.Closeds.uniformSpace toCloseds	—	IsUniformEmbedding.isEmbedding isUniformEmbedding_toCloseds
isUniformEmbedding_coe 📖	mathematical	—	IsUniformEmbedding TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace Set uniformSpace UniformSpace.hausdorff SetLike.coe instSetLike	—	SetLike.coe_injective
isUniformEmbedding_singleton 📖	mathematical	—	IsUniformEmbedding TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace uniformSpace instSingleton	—	IsUniformEmbedding.of_comp_iff isUniformEmbedding_coe UniformSpace.hausdorff.isUniformEmbedding_singleton
isUniformEmbedding_toCloseds 📖	mathematical	—	IsUniformEmbedding TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace TopologicalSpace.Closeds uniformSpace TopologicalSpace.Closeds.uniformSpace toCloseds	—	Filter.comap_comap toCloseds_injective
isUniformEmbedding_toCompacts 📖	mathematical	—	IsUniformEmbedding TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace TopologicalSpace.Compacts uniformSpace TopologicalSpace.Compacts.uniformSpace toCompacts	—	Filter.comap_comap toCompacts_injective
totallyBounded_subsets_of_totallyBounded 📖	mathematical	TotallyBounded	TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace uniformSpace setOf Set Set.instHasSubset SetLike.coe instSetLike	—	totallyBounded_preimage IsUniformEmbedding.isUniformInducing isUniformEmbedding_coe TotallyBounded.powerset_hausdorff
uniformContinuous_coe 📖	mathematical	—	UniformContinuous TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace Set uniformSpace UniformSpace.hausdorff SetLike.coe instSetLike	—	IsUniformInducing.uniformContinuous IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_coe
uniformContinuous_singleton 📖	mathematical	—	UniformContinuous TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace uniformSpace instSingleton	—	IsUniformInducing.uniformContinuous IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_singleton
uniformContinuous_sup 📖	mathematical	—	UniformContinuous TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace instUniformSpaceProd uniformSpace instMax	—	IsUniformInducing.uniformContinuous_iff IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_coe UniformContinuous.comp UniformSpace.hausdorff.uniformContinuous_union UniformContinuous.prodMap uniformContinuous_coe
uniformContinuous_toCloseds 📖	mathematical	—	UniformContinuous TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace TopologicalSpace.Closeds uniformSpace TopologicalSpace.Closeds.uniformSpace toCloseds	—	IsUniformInducing.uniformContinuous IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_toCloseds
uniformContinuous_toCompacts 📖	mathematical	—	UniformContinuous TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace TopologicalSpace.Compacts uniformSpace TopologicalSpace.Compacts.uniformSpace toCompacts	—	IsUniformInducing.uniformContinuous IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_toCompacts
uniformity_def 📖	mathematical	—	uniformity TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace uniformSpace Filter.comap Set SetLike.coe instSetLike Filter.lift' hausdorffEntourage	—	—

TotallyBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_prodMk_finset_mem_hausdorffEntourage 📖	mathematical	TotallyBounded SetRel Filter Filter.instMembership uniformity	Set Set.instMembership hausdorffEntourage SetLike.coe Finset Finset.instSetLike	—	symm_le_uniformity CanLift.prf Set.instCanLiftFinsetCoeFinite Finset.coe_filter Set.mem_iUnion₂
nhds_vietoris_le_nhds_hausdorff 📖	mathematical	TotallyBounded	Filter Set Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds TopologicalSpace.vietoris UniformSpace.toTopologicalSpace UniformSpace.hausdorff	—	nhds_eq_comap_uniformity Filter.HasBasis.ge_iff Filter.HasBasis.comap Filter.HasBasis.uniformity_hausdorff uniformity_hasBasis_open refl_mem_uniformity Filter.inter_mem comp_open_symm_mem_uniformity_sets exists_prodMk_finset_mem_hausdorffEntourage Filter.mp_mem Filter.eventually_all_finset IsOpen.eventually_mem TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen UniformSpace.isOpen_ball Filter.univ_mem' Mathlib.Tactic.GCongr.rel_imp_rel Set.instIsTransSubset subset_refl Set.instReflSubset SetRel.preimage_eq_image SetRel.preimage_subset_preimage SetRel.preimage_subset_preimage_left SetRel.preimage_comp IsOpen.mem_nhds IsOpen.powerset_vietoris IsOpen.relImage SetRel.self_subset_image
powerset_hausdorff 📖	mathematical	TotallyBounded	Set UniformSpace.hausdorff Set.powerset	—	Filter.HasBasis.totallyBounded_iff Filter.HasBasis.uniformity_hausdorff Filter.basis_sets Set.iUnion_congr_Prop Set.Finite.powerset Set.mem_iUnion₂

UniformContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compacts_map 📖	mathematical	UniformContinuous	TopologicalSpace.Compacts UniformSpace.toTopologicalSpace TopologicalSpace.Compacts.uniformSpace TopologicalSpace.Compacts.map continuous	—	continuous IsUniformInducing.uniformContinuous_iff IsUniformEmbedding.toIsUniformInducing TopologicalSpace.Compacts.isUniformEmbedding_coe comp image_hausdorff TopologicalSpace.Compacts.uniformContinuous_coe
image_hausdorff 📖	mathematical	UniformContinuous	Set UniformSpace.hausdorff Set.image	—	Filter.tendsto_lift' Filter.mp_mem Filter.mem_lift' Filter.univ_mem' HasSubset.Subset.trans Set.instIsTransSubset Set.mem_image_of_mem
nonemptyCompacts_map 📖	mathematical	UniformContinuous	TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace TopologicalSpace.NonemptyCompacts.uniformSpace TopologicalSpace.NonemptyCompacts.map continuous	—	continuous IsUniformInducing.uniformContinuous_iff IsUniformEmbedding.toIsUniformInducing TopologicalSpace.NonemptyCompacts.isUniformEmbedding_coe comp image_hausdorff TopologicalSpace.NonemptyCompacts.uniformContinuous_coe
sup_closeds 📖	mathematical	UniformContinuous TopologicalSpace.Closeds UniformSpace.toTopologicalSpace TopologicalSpace.Closeds.uniformSpace	SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Closeds.instCompleteLattice	—	comp TopologicalSpace.Closeds.uniformContinuous_sup prodMk
sup_compacts 📖	mathematical	UniformContinuous TopologicalSpace.Compacts UniformSpace.toTopologicalSpace TopologicalSpace.Compacts.uniformSpace	TopologicalSpace.Compacts.instMax	—	comp TopologicalSpace.Compacts.uniformContinuous_sup prodMk
sup_nonemptyCompacts 📖	mathematical	UniformContinuous TopologicalSpace.NonemptyCompacts UniformSpace.toTopologicalSpace TopologicalSpace.NonemptyCompacts.uniformSpace	TopologicalSpace.NonemptyCompacts.instMax	—	comp TopologicalSpace.NonemptyCompacts.uniformContinuous_sup prodMk

UniformSpace

Definitions

Name	Category	Theorems
hausdorff 📖	CompOp	29 math math: TopologicalSpace.Closeds.uniformContinuous_closure, hausdorff.isClopen_singleton_empty, UniformContinuous.image_hausdorff, TopologicalSpace.Closeds.isUniformEmbedding_coe, hausdorff.isUniformEmbedding_singleton, TopologicalSpace.Closeds.continuous_closure, hausdorff.uniformContinuous_closure, hausdorff.isClosedEmbedding_singleton, hausdorff.nhds_closure, TopologicalSpace.NonemptyCompacts.uniformContinuous_coe, hausdorff.isOpen_inter_nonempty_of_isOpen, Filter.HasBasis.uniformity_hausdorff, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_coe, hausdorff.isUniformInducing_closure, hausdorff.uniformContinuous_union, TopologicalSpace.Compacts.uniformContinuous_coe, TopologicalSpace.Compacts.isUniformEmbedding_coe, hausdorff.instCompactSpaceSet, hausdorff.continuous_closure, TotallyBounded.nhds_vietoris_le_nhds_hausdorff, hausdorff.instDiscreteUniformitySet, TotallyBounded.powerset_hausdorff, TopologicalSpace.Closeds.uniformContinuous_coe, TopologicalSpace.Closeds.isUniformInducing_closure, hausdorff.isClosed_powerset, IsUniformInducing.image_hausdorff, IsCompact.nhds_hausdorff_eq_nhds_vietoris, IsClosed.powerset_hausdorff, IsUniformEmbedding.image_hausdorff

UniformSpace.hausdorff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_closure 📖	mathematical	—	Continuous Set UniformSpace.toTopologicalSpace UniformSpace.hausdorff closure	—	UniformContinuous.continuous uniformContinuous_closure
instCompactSpaceSet 📖	mathematical	—	CompactSpace Set UniformSpace.toTopologicalSpace UniformSpace.hausdorff	—	isCompact_iff_ultrafilter_le_nhds Set.mem_univ IsCompact.nhds_hausdorff_eq_nhds_vietoris IsClosed.isCompact isClosed_closure le_imp_le_of_le_of_le le_refl Specializes.nhds_le_nhds TopologicalSpace.vietoris.specializes_closure Ultrafilter.le_nhds_lim TopologicalSpace.vietoris.instCompactSpaceSet
instDiscreteUniformitySet 📖	mathematical	—	DiscreteUniformity Set UniformSpace.hausdorff	—	discreteUniformity_iff_setRelId_mem_uniformity hausdorffEntourage_id Filter.mem_lift' DiscreteUniformity.relId_mem_uniformity
isClopen_singleton_empty 📖	mathematical	—	IsClopen Set UniformSpace.toTopologicalSpace UniformSpace.hausdorff Set.instSingletonSet Set.instEmptyCollection	—	Set.powerset_empty IsClosed.powerset_hausdorff isClosed_empty nhds_eq_uniformity Filter.mp_mem Filter.mem_lift' Filter.univ_mem Filter.univ_mem' SetRel.image_empty_right
isClosedEmbedding_singleton 📖	mathematical	—	Topology.IsClosedEmbedding Set UniformSpace.toTopologicalSpace UniformSpace.hausdorff Set.instSingletonSet	—	IsUniformEmbedding.isEmbedding isUniformEmbedding_singleton isOpen_compl_iff isOpen_iff_mem_nhds Set.eq_empty_or_nonempty isOpen_singleton_iff_nhds_eq_pure IsClopen.isOpen isClopen_singleton_empty Filter.mem_pure Set.Nonempty.exists_eq_singleton_or_nontrivial Set.mem_range_self t2_separation T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace Filter.mp_mem IsOpen.mem_nhds IsOpen.inter isOpen_inter_nonempty_of_isOpen Filter.univ_mem' Disjoint.notMem_of_mem_left Set.singleton_inter_nonempty Set.mem_setOf
isClosed_powerset 📖	mathematical	—	IsClosed Set UniformSpace.toTopologicalSpace UniformSpace.hausdorff Set.powerset	—	IsClosed.powerset_hausdorff
isOpen_inter_nonempty_of_isOpen 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace	Set UniformSpace.hausdorff setOf Set.Nonempty Set.instInter	—	isOpen_iff_mem_nhds UniformSpace.mem_nhds_iff IsOpen.mem_nhds_iff Filter.mem_lift'
isUniformEmbedding_singleton 📖	mathematical	—	IsUniformEmbedding Set UniformSpace.hausdorff Set.instSingletonSet	—	Filter.comap_lift'_eq Filter.lift'_id Set.singleton_injective
isUniformInducing_closure 📖	mathematical	—	IsUniformInducing Set UniformSpace.hausdorff closure UniformSpace.toTopologicalSpace	—	le_antisymm Filter.HasBasis.le_basis_iff Filter.HasBasis.comap Filter.HasBasis.uniformity_hausdorff Filter.basis_sets comp_mem_uniformity_sets Mathlib.Tactic.GCongr.rel_imp_rel Set.instIsTransSubset subset_closure subset_refl Set.instReflSubset SetRel.preimage_subset_preimage UniformSpace.closure_subset_preimage SetRel.preimage_subset_preimage_left SetRel.preimage_comp SetRel.image_subset_image UniformSpace.closure_subset_image SetRel.image_subset_image_left SetRel.image_comp Filter.map_le_iff_le_comap uniformContinuous_closure
nhds_closure 📖	mathematical	—	nhds Set UniformSpace.toTopologicalSpace UniformSpace.hausdorff closure	—	Topology.IsInducing.nhds_eq_comap IsUniformInducing.isInducing isUniformInducing_closure closure_closure
uniformContinuous_closure 📖	mathematical	—	UniformContinuous Set UniformSpace.hausdorff closure UniformSpace.toTopologicalSpace	—	Filter.HasBasis.tendsto_iff Filter.HasBasis.uniformity_hausdorff Filter.basis_sets comp_mem_uniformity_sets Mathlib.Tactic.GCongr.rel_imp_rel Set.instIsTransSubset UniformSpace.closure_subset_preimage subset_refl Set.instReflSubset SetRel.preimage_subset_preimage subset_closure SetRel.preimage_subset_preimage_left SetRel.preimage_comp UniformSpace.closure_subset_image SetRel.image_subset_image SetRel.image_subset_image_left SetRel.image_comp
uniformContinuous_union 📖	mathematical	—	UniformContinuous Set instUniformSpaceProd UniformSpace.hausdorff Set.instUnion	—	Filter.tendsto_lift' Filter.mp_mem entourageProd_mem_uniformity Filter.mem_lift' Filter.univ_mem' union_mem_hausdorffEntourage

(root)

Definitions

Name	Category	Theorems
hausdorffEntourage 📖	CompOp	20 math math: isTrans_hausdorffEntourage, monotone_hausdorffEntourage, Filter.HasBasis.uniformity_nonemptyCompacts, TotallyBounded.exists_prodMk_finset_mem_hausdorffEntourage, Filter.HasBasis.uniformity_closeds, TopologicalSpace.Closeds.uniformity_def, TopologicalSpace.NonemptyCompacts.uniformity_def, TopologicalSpace.Compacts.uniformity_def, Filter.HasBasis.uniformity_compacts, Filter.HasBasis.uniformity_hausdorff, EMetric.mem_hausdorffEntourage_of_hausdorffEdist_lt, hausdorffEntourage_comp, inv_hausdorffEntourage, mem_hausdorffEntourage, isSymm_hausdorffEntourage, hausdorffEntourage_id, hausdorffEntourage_mono, isRefl_hausdorffEntourage, Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt, singleton_mem_hausdorffEntourage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hausdorffEntourage_comp 📖	mathematical	—	hausdorffEntourage SetRel.comp Set	—	subset_antisymm Set.instAntisymmSubset Set.inter_subset_left Set.inter_subset_right mem_hausdorffEntourage SetRel.preimage_comp Mathlib.Tactic.GCongr.rel_imp_rel Set.instIsTransSubset subset_refl Set.instReflSubset SetRel.preimage_subset_preimage SetRel.image_comp Mathlib.Tactic.GCongr.and_right_mono SetRel.image_subset_image subset_rfl
hausdorffEntourage_id 📖	mathematical	—	hausdorffEntourage SetRel.id Set	—	SetRel.preimage_id SetRel.image_id Set.instReflSubset Set.instAntisymmSubset
hausdorffEntourage_mono 📖	mathematical	SetRel Set.instHasSubset	Set hausdorffEntourage	—	Set.setOf_subset_setOf_of_imp Mathlib.Tactic.GCongr.rel_imp_rel Set.instIsTransSubset subset_refl Set.instReflSubset SetRel.preimage_subset_preimage_left SetRel.image_subset_image_left
inv_hausdorffEntourage 📖	mathematical	—	SetRel.inv Set hausdorffEntourage	—	Set.ext
isRefl_hausdorffEntourage 📖	mathematical	—	SetRel.IsRefl Set hausdorffEntourage	—	SetRel.self_subset_preimage SetRel.self_subset_image
isSymm_hausdorffEntourage 📖	mathematical	—	SetRel.IsSymm Set hausdorffEntourage	—	SetRel.inv_eq_self_iff inv_hausdorffEntourage SetRel.inv_eq_self
isTrans_hausdorffEntourage 📖	mathematical	—	SetRel.IsTrans Set hausdorffEntourage	—	SetRel.isTrans_iff_comp_subset_self hausdorffEntourage_comp Mathlib.Tactic.GCongr.rel_imp_rel Set.instIsTransSubset hausdorffEntourage_mono SetRel.comp_subset_self subset_refl Set.instReflSubset
mem_hausdorffEntourage 📖	mathematical	—	Set SetRel Set.instMembership hausdorffEntourage Set.instHasSubset SetRel.preimage SetRel.image	—	—
monotone_hausdorffEntourage 📖	mathematical	—	Monotone SetRel Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra hausdorffEntourage	—	hausdorffEntourage_mono
singleton_mem_hausdorffEntourage 📖	mathematical	—	Set SetRel Set.instMembership hausdorffEntourage Set.instSingletonSet	—	—
union_mem_hausdorffEntourage 📖	mathematical	Set SetRel Set.instMembership hausdorffEntourage	Set.instUnion	—	—

---

← Back to Index