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_prod`, `continuous_singleton`, `discreteUniformity_iff`, `instCompactSpace`, `instContinuousSup`, `instDiscreteUniformity`, `instNoncompactSpace`, `instT0Space`, `isClopen_singleton_bot`, `isClosedEmbedding_singleton`, `isClosed_setOf_totallyBounded`, `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_prod`, `uniformContinuous_singleton`, `uniformContinuous_sup`, `uniformity_def`, `completeSpace_iff`, `continuous_toCloseds`, `discreteUniformity_iff`, `instCompleteSpace`, `instDiscreteUniformity`, `isClosedEmbedding_toCloseds`, `isEmbedding_toCloseds`, `isUniformEmbedding_coe`, `isUniformEmbedding_singleton`, `isUniformEmbedding_toCloseds`, `totallyBounded_subsets_of_totallyBounded`, `uniformContinuous_coe`, `uniformContinuous_prod`, `uniformContinuous_singleton`, `uniformContinuous_sup`, `uniformContinuous_toCloseds`, `uniformity_def`, `completeSpace_iff`, `continuous_toCloseds`, `discreteUniformity_iff`, `instCompleteSpace`, `instDiscreteUniformity`, `isClosedEmbedding_toCloseds`, `isEmbedding_toCloseds`, `isUniformEmbedding_coe`, `isUniformEmbedding_singleton`, `isUniformEmbedding_toCloseds`, `isUniformEmbedding_toCompacts`, `totallyBounded_subsets_of_totallyBounded`, `uniformContinuous_coe`, `uniformContinuous_prod`, `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`, `prod_closeds`, `prod_compacts`, `prod_nonemptyCompacts`, `sup_closeds`, `sup_compacts`, `sup_nonemptyCompacts`, `continuous_closure`, `instCompactSpaceSet`, `instDiscreteUniformitySet`, `isClopen_singleton_empty`, `isClosedEmbedding_singleton`, `isClosed_powerset`, `isClosed_setOf_totallyBounded`, `isOpen_inter_nonempty_of_isOpen`, `isUniformEmbedding_singleton`, `isUniformInducing_closure`, `nhds_closure`, `uniformContinuous_closure`, `uniformContinuous_prod`, `uniformContinuous_union`, `hausdorffEntourage_comp`, `hausdorffEntourage_id`, `hausdorffEntourage_mono`, `inv_hausdorffEntourage`, `isRefl_hausdorffEntourage`, `isSymm_hausdorffEntourage`, `isTrans_hausdorffEntourage`, `mem_hausdorffEntourage`, `monotone_hausdorffEntourage`, `prod_mem_hausdorffEntourage_entourageProd`, `singleton_mem_hausdorffEntourage`, `union_mem_hausdorffEntourage`	113
Total	120

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`	`Filter.HasBasis` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `uniformity` `TopologicalSpace.Closeds.uniformSpace` `Set.preimage` `Set` `SetLike.coe` `TopologicalSpace.Closeds.instSetLike` `hausdorffEntourage`	—	`comap` `uniformity_hausdorff`
`uniformity_compacts` 📖	mathematical	`Filter.HasBasis` `uniformity`	`Filter.HasBasis` `TopologicalSpace.Compacts` `UniformSpace.toTopologicalSpace` `uniformity` `TopologicalSpace.Compacts.uniformSpace` `Set.preimage` `Set` `SetLike.coe` `TopologicalSpace.Compacts.instSetLike` `hausdorffEntourage`	—	`comap` `uniformity_hausdorff`
`uniformity_hausdorff` 📖	mathematical	`Filter.HasBasis` `uniformity`	`Filter.HasBasis` `Set` `uniformity` `UniformSpace.hausdorff` `SetRel` `hausdorffEntourage`	—	`lift'` `monotone_hausdorffEntourage`
`uniformity_nonemptyCompacts` 📖	mathematical	`Filter.HasBasis` `uniformity`	`Filter.HasBasis` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `uniformity` `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.toTopologicalSpace` `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`	`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`	`IsUniformEmbedding` `Set` `UniformSpace.hausdorff` `Set.image`	—	`IsUniformInducing.image_hausdorff` `isUniformInducing` `Function.Injective.image_injective` `injective`
`nonemptyCompacts_map` 📖	mathematical	`IsUniformEmbedding`	`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`	`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`	`IsUniformInducing` `Set` `UniformSpace.hausdorff` `Set.image`	—	`Filter.comap_lift'_eq` `comap_uniformity` `Filter.comap_lift'_eq2` `monotone_hausdorffEntourage` `Set.ext`
`nonemptyCompacts_map` 📖	mathematical	`IsUniformInducing`	`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	158 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`, `NonemptyCompacts.toCloseds_prod`, `NoetherianSpace.exists_finset_irreducible`, `UniformContinuous.sup_closeds`, `Closeds.coe_preimage`, `Closeds.singleton_inj`, `Closeds.gc`, `Closeds.continuous_closure`, `Compacts.toCloseds_prod`, `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`, `Closeds.isClosed_setOf_totallyBounded`, `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`, `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`, `UniformContinuous.prod_closeds`, `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`, `AlgebraicGeometry.Scheme.irreducibleComponentι_apply`, `Closeds.isAtom_iff`, `AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal`, `NonemptyCompacts.isometry_toCloseds`, `NonemptyCompacts.isClosedEmbedding_toCloseds`, `noetherianSpace_TFAE`, `AlgebraicGeometry.Scheme.IdealSheafData.support_iSup`, `Closeds.instCompleteSpace`, `Closeds.lipschitz_prod`, `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`, `Compacts.isClosedEmbedding_toCloseds`, `Clopens.coe_toCloseds`, `Closeds.mem_prod`, `Closeds.isAtom_coe`, `Closeds.mem_closure`, `Closeds.singleton_prod_singleton`, `AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top`, `Closeds.totallyBounded_subsets_of_totallyBounded`, `NonemptyCompacts.continuous_toCloseds`, `AlgebraicGeometry.Scheme.Hom.range_subset_ker_support`, `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.coe_prod`, `Closeds.continuous_prod`, `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`, `Closeds.coe_eq_singleton_of_isAtom`, `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.uniformContinuous_prod`, `Closeds.instT0Space`, `Closeds.isOpen_inter_nonempty_of_isOpen`

TopologicalSpace.Closeds

Definitions

Name	Category	Theorems
`uniformSpace` 📖	CompOp	48 math math: `TopologicalSpace.NonemptyCompacts.uniformContinuous_toCloseds`, `uniformContinuous_closure`, `noncompactSpace_iff`, `EMetric.NonemptyCompacts.isUniformEmbedding_toCloseds`, `isUniformEmbedding_coe`, `TopologicalSpace.NonemptyCompacts.isClosed_in_closeds`, `instContinuousSup`, `UniformContinuous.sup_closeds`, `continuous_closure`, `Filter.HasBasis.uniformity_closeds`, `uniformity_def`, `isClosed_setOf_totallyBounded`, `instNoncompactSpace`, `TopologicalSpace.NonemptyCompacts.isEmbedding_toCloseds`, `TopologicalSpace.Compacts.uniformContinuous_toCloseds`, `TopologicalSpace.Compacts.isUniformEmbedding_toCloseds`, `UniformContinuous.prod_closeds`, `isClosed_subsets_of_isClosed`, `instCompactSpace`, `TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds`, `instDiscreteUniformity`, `continuous_infEDist`, `TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCloseds`, `instCompleteSpace`, `continuous_singleton`, `EMetric.NonemptyCompacts.isClosed_in_closeds`, `TopologicalSpace.Compacts.continuous_toCloseds`, `isClopen_singleton_bot`, `TopologicalSpace.Compacts.isClosedEmbedding_toCloseds`, `totallyBounded_subsets_of_totallyBounded`, `TopologicalSpace.NonemptyCompacts.continuous_toCloseds`, `isUniformEmbedding_singleton`, `compactSpace_iff`, `uniformContinuous_sup`, `TopologicalSpace.Compacts.isEmbedding_toCloseds`, `continuous_prod`, `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`, `uniformContinuous_prod`, `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_prod` 📖	mathematical	—	`Continuous` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `instTopologicalSpaceProd` `uniformSpace` `instUniformSpaceProd` `SProd.sprod` `instSProdProd`	—	`UniformContinuous.continuous` `uniformContinuous_prod`
`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_setOf_totallyBounded` 📖	mathematical	—	`IsClosed` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `uniformSpace` `setOf` `TotallyBounded` `SetLike.coe` `instSetLike`	—	`IsClosed.preimage` `UniformContinuous.continuous` `uniformContinuous_coe` `UniformSpace.hausdorff.isClosed_setOf_totallyBounded`
`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`	`IsOpen` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `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.of_comp_iff` `IsUniformEmbedding.isUniformInducing` `isUniformEmbedding_coe` `UniformSpace.hausdorff.isUniformInducing_closure`
`noncompactSpace_iff` 📖	mathematical	—	`NoncompactSpace` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `uniformSpace`	—	—
`totallyBounded_subsets_of_totallyBounded` 📖	mathematical	`TotallyBounded`	`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_prod` 📖	mathematical	—	`UniformContinuous` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `instTopologicalSpaceProd` `instUniformSpaceProd` `uniformSpace` `SProd.sprod` `instSProdProd`	—	`IsUniformInducing.uniformContinuous_iff` `IsUniformEmbedding.toIsUniformInducing` `isUniformEmbedding_coe` `UniformContinuous.comp` `UniformSpace.hausdorff.uniformContinuous_prod` `UniformContinuous.prodMap` `uniformContinuous_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	22 math math: `completeSpace_iff`, `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`, `UniformContinuous.sup_compacts`, `instCompleteSpace`, `TopologicalSpace.NonemptyCompacts.uniformContinuous_toCompacts`, `UniformContinuous.prod_compacts`, `uniformContinuous_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace_iff` 📖	mathematical	—	`CompleteSpace` `TopologicalSpace.Compacts` `UniformSpace.toTopologicalSpace` `uniformSpace`	—	`TopologicalSpace.NonemptyCompacts.completeSpace_iff` `IsUniformInducing.completeSpace` `IsUniformEmbedding.toIsUniformInducing` `TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCompacts` `IsClosed.isComplete` `Topology.IsClosedEmbedding.isClosed_range` `TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCompacts` `instCompleteSpace`
`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`
`instCompleteSpace` 📖	mathematical	—	`CompleteSpace` `TopologicalSpace.Compacts` `UniformSpace.toTopologicalSpace` `uniformSpace`	—	`comp_mem_uniformity_sets` `Filter.Eventually.exists` `symm_le_uniformity` `IsCompact.totallyBounded` `isCompact` `Filter.mem_of_superset` `Filter.mem_lift'` `Set.iUnion₂_subset_iff` `Mathlib.Tactic.GCongr.rel_imp_rel` `Set.instIsTransSubset` `subset_refl` `Set.instReflSubset` `SetRel.preimage_subset_preimage_left` `SetRel.preimage_comp` `SetRel.preimage_subset_preimage` `SetRel.preimage_eq_biUnion` `Filter.TotallyBounded.isCompact_setOf_clusterPt` `nhds_eq_comap_uniformity'` `Filter.HasBasis.ge_iff` `Filter.HasBasis.comap` `Filter.HasBasis.uniformity_compacts` `uniformity_hasBasis_closed` `Filter.mp_mem` `Filter.univ_mem'` `Filter.TotallyBounded.mono` `inf_le_left` `Filter.lift'_inf_principal_eq` `Filter.lift'_neBot_iff` `Set.inter_subset_inter_left` `Set.biUnion_subset_biUnion_left` `Filter.nonempty_of_mem` `Filter.inter_mem` `Set.mem_iUnion₂_of_mem` `Filter.TotallyBounded.exists_clusterPt` `ClusterPt.of_inf_left` `ClusterPt.of_inf_right` `IsClosed.closure_eq` `UniformSpace.isClosed_ball` `mem_closure_iff_clusterPt` `IsClosed.relImage_of_isCompact` `ClusterPt.mono` `Filter.le_principal_iff` `Filter.basis_sets` `le_imp_le_of_le_of_le` `Filter.curry_le_prod` `le_refl`
`instDiscreteUniformity` 📖	mathematical	—	`DiscreteUniformity` `TopologicalSpace.Compacts` `UniformSpace.toTopologicalSpace` `uniformSpace`	—	`IsUniformEmbedding.discreteUniformity` `UniformSpace.hausdorff.instDiscreteUniformitySet` `isUniformEmbedding_coe`
`isClosedEmbedding_toCloseds` 📖	mathematical	—	`Topology.IsClosedEmbedding` `TopologicalSpace.Compacts` `UniformSpace.toTopologicalSpace` `TopologicalSpace.Closeds` `topology` `TopologicalSpace.Closeds.uniformSpace` `toCloseds`	—	`isEmbedding_toCloseds` `subset_antisymm` `Set.instAntisymmSubset` `Set.range_subset_iff` `IsCompact.totallyBounded` `isCompact` `TotallyBounded.isCompact_of_isClosed` `TopologicalSpace.Closeds.isClosed` `TopologicalSpace.Closeds.isClosed_setOf_totallyBounded`
`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`	`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_prod` 📖	mathematical	—	`UniformContinuous` `TopologicalSpace.Compacts` `UniformSpace.toTopologicalSpace` `instTopologicalSpaceProd` `instUniformSpaceProd` `uniformSpace` `SProd.sprod` `instSProdProd`	—	`IsUniformInducing.uniformContinuous_iff` `IsUniformEmbedding.toIsUniformInducing` `isUniformEmbedding_coe` `UniformContinuous.comp` `UniformSpace.hausdorff.uniformContinuous_prod` `UniformContinuous.prodMap` `uniformContinuous_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	24 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`, `completeSpace_iff`, `isUniformEmbedding_coe`, `isUniformEmbedding_toCloseds`, `totallyBounded_subsets_of_totallyBounded`, `isUniformEmbedding_toCompacts`, `isUniformEmbedding_singleton`, `uniformContinuous_prod`, `instCompleteSpace`, `discreteUniformity_iff`, `UniformContinuous.nonemptyCompacts_map`, `uniformContinuous_toCompacts`, `UniformContinuous.sup_nonemptyCompacts`, `UniformContinuous.prod_nonemptyCompacts`, `IsUniformInducing.nonemptyCompacts_map`, `IsUniformEmbedding.nonemptyCompacts_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace_iff` 📖	mathematical	—	`CompleteSpace` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `uniformSpace`	—	`CompleteSpace.complete` `Cauchy.map` `uniformContinuous_singleton` `nonempty` `Filter.HasBasis.ge_iff` `nhds_basis_opens` `Filter.mp_mem` `IsOpen.mem_nhds` `isOpen_inter_nonempty_of_isOpen` `Filter.univ_mem'` `instCompleteSpace`
`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`
`instCompleteSpace` 📖	mathematical	—	`CompleteSpace` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `uniformSpace`	—	`IsUniformInducing.completeSpace` `IsUniformEmbedding.toIsUniformInducing` `isUniformEmbedding_toCompacts` `IsClosed.isComplete` `TopologicalSpace.Compacts.instCompleteSpace` `Topology.IsClosedEmbedding.isClosed_range` `isClosedEmbedding_toCompacts`
`instDiscreteUniformity` 📖	mathematical	—	`DiscreteUniformity` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `uniformSpace`	—	`IsUniformEmbedding.discreteUniformity` `UniformSpace.hausdorff.instDiscreteUniformitySet` `isUniformEmbedding_coe`
`isClosedEmbedding_toCloseds` 📖	mathematical	—	`Topology.IsClosedEmbedding` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `TopologicalSpace.Closeds` `topology` `TopologicalSpace.Closeds.uniformSpace` `toCloseds`	—	`Topology.IsClosedEmbedding.comp` `TopologicalSpace.Compacts.isClosedEmbedding_toCloseds` `isClosedEmbedding_toCompacts`
`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`	`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_prod` 📖	mathematical	—	`UniformContinuous` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `instTopologicalSpaceProd` `instUniformSpaceProd` `uniformSpace` `SProd.sprod` `instSProdProd`	—	`IsUniformInducing.uniformContinuous_iff` `IsUniformEmbedding.toIsUniformInducing` `isUniformEmbedding_coe` `UniformContinuous.comp` `UniformSpace.hausdorff.uniformContinuous_prod` `UniformContinuous.prodMap` `uniformContinuous_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`	`Finset` `Set` `SetRel` `Set.instMembership` `hausdorffEntourage` `SetLike.coe` `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`	`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`	`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`	`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`	`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`
`prod_closeds` 📖	mathematical	`UniformContinuous` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `TopologicalSpace.Closeds.uniformSpace`	`UniformContinuous` `TopologicalSpace.Closeds` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `TopologicalSpace.Closeds.uniformSpace` `instUniformSpaceProd` `SProd.sprod` `TopologicalSpace.Closeds.instSProdProd`	—	`comp` `TopologicalSpace.Closeds.uniformContinuous_prod` `prodMk`
`prod_compacts` 📖	mathematical	`UniformContinuous` `TopologicalSpace.Compacts` `UniformSpace.toTopologicalSpace` `TopologicalSpace.Compacts.uniformSpace`	`UniformContinuous` `TopologicalSpace.Compacts` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `TopologicalSpace.Compacts.uniformSpace` `instUniformSpaceProd` `SProd.sprod` `TopologicalSpace.Compacts.instSProdProd`	—	`comp` `TopologicalSpace.Compacts.uniformContinuous_prod` `prodMk`
`prod_nonemptyCompacts` 📖	mathematical	`UniformContinuous` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `TopologicalSpace.NonemptyCompacts.uniformSpace`	`UniformContinuous` `TopologicalSpace.NonemptyCompacts` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `TopologicalSpace.NonemptyCompacts.uniformSpace` `instUniformSpaceProd` `SProd.sprod` `TopologicalSpace.NonemptyCompacts.instSProdProd`	—	`comp` `TopologicalSpace.NonemptyCompacts.uniformContinuous_prod` `prodMk`
`sup_closeds` 📖	mathematical	`UniformContinuous` `TopologicalSpace.Closeds` `UniformSpace.toTopologicalSpace` `TopologicalSpace.Closeds.uniformSpace`	`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`	`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`	`UniformContinuous` `TopologicalSpace.NonemptyCompacts` `UniformSpace.toTopologicalSpace` `TopologicalSpace.NonemptyCompacts.uniformSpace` `TopologicalSpace.NonemptyCompacts.instMax`	—	`comp` `TopologicalSpace.NonemptyCompacts.uniformContinuous_sup` `prodMk`

UniformSpace

Definitions

Name	Category	Theorems
`hausdorff` 📖	CompOp	31 math math: `TopologicalSpace.Closeds.uniformContinuous_closure`, `hausdorff.isClosed_setOf_totallyBounded`, `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_prod`, `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`
`isClosed_setOf_totallyBounded` 📖	mathematical	—	`IsClosed` `Set` `UniformSpace.toTopologicalSpace` `UniformSpace.hausdorff` `setOf` `TotallyBounded`	—	`nhds_eq_comap_uniformity` `comp_mem_uniformity_sets` `Filter.HasBasis.frequently_iff` `Filter.HasBasis.comap` `Filter.HasBasis.uniformity_hausdorff` `Filter.basis_sets` `Mathlib.Tactic.GCongr.rel_imp_rel` `Set.instIsTransSubset` `subset_refl` `Set.instReflSubset` `SetRel.preimage_subset_preimage` `Set.iUnion_mono''` `Set.setOf_subset_setOf_of_imp` `Set.mem_of_subset_of_mem` `Set.iUnion_congr_Prop`
`isOpen_inter_nonempty_of_isOpen` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace`	`IsOpen` `Set` `UniformSpace.toTopologicalSpace` `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_prod` 📖	mathematical	—	`UniformContinuous` `Set` `instUniformSpaceProd` `UniformSpace.hausdorff` `SProd.sprod` `Set.instSProd`	—	`Filter.HasBasis.tendsto_right_iff` `Filter.HasBasis.lift'` `Filter.HasBasis.uniformity_prod` `Filter.basis_sets` `monotone_hausdorffEntourage` `Filter.mp_mem` `entourageProd_mem_uniformity` `Filter.mem_lift'` `Filter.univ_mem'` `prod_mem_hausdorffEntourage_entourageProd`
`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	22 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`, `union_mem_hausdorffEntourage`, `Filter.HasBasis.uniformity_hausdorff`, `EMetric.mem_hausdorffEntourage_of_hausdorffEdist_lt`, `hausdorffEntourage_comp`, `inv_hausdorffEntourage`, `mem_hausdorffEntourage`, `isSymm_hausdorffEntourage`, `hausdorffEntourage_id`, `hausdorffEntourage_mono`, `prod_mem_hausdorffEntourage_entourageProd`, `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`	`SetRel` `Set` `Set.instHasSubset` `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`
`prod_mem_hausdorffEntourage_entourageProd` 📖	mathematical	`Set` `SetRel` `Set.instMembership` `hausdorffEntourage`	`Set` `SetRel` `Set.instMembership` `hausdorffEntourage` `entourageProd` `SProd.sprod` `Set.instSProd`	—	—
`singleton_mem_hausdorffEntourage` 📖	mathematical	—	`Set` `SetRel` `Set.instMembership` `hausdorffEntourage` `Set.instSingletonSet`	—	—
`union_mem_hausdorffEntourage` 📖	mathematical	`Set` `SetRel` `Set.instMembership` `hausdorffEntourage`	`Set` `SetRel` `Set.instMembership` `hausdorffEntourage` `Set.instUnion`	—	—

---

← Back to Index