Hausdorff uniformity #
This file defines the Hausdorff uniformity on the types of closed subsets, compact subsets and and nonempty compact subsets of a uniform space. This is the generalization of the uniformity induced by the Hausdorff metric to hyperspaces of uniform spaces.
The set of pairs of sets contained in each other's thickening with respect to an entourage.
Equations
Instances For
@[simp]
@[simp]
theorem
TotallyBounded.exists_prodMk_finset_mem_hausdorffEntourage
{α : Type u_1}
[UniformSpace α]
{s : Set α}
(hs : TotallyBounded s)
{U : SetRel α α}
(hU : U ∈ uniformity α)
:
@[reducible, inline]
The Hausdorff uniformity on the powerset of a uniform space. Used for defining the uniformities
on Closeds, Compacts and NonemptyCompacts.
See note [reducible non-instances].
Equations
Instances For
theorem
Filter.HasBasis.uniformity_hausdorff
{α : Type u_1}
[UniformSpace α]
{ι : Sort u_3}
{p : ι → Prop}
{s : ι → Set (α × α)}
(h : (uniformity α).HasBasis p s)
:
(uniformity (Set α)).HasBasis p (hausdorffEntourage ∘ s)
In the Hausdorff uniformity, the powerset of a closed set is closed.
@[deprecated IsClosed.powerset_hausdorff (since := "2025-11-23")]
theorem
UniformSpace.hausdorff.isClosed_powerset
{α : Type u_1}
[UniformSpace α]
{F : Set α}
(hF : IsClosed F)
:
Alias of IsClosed.powerset_hausdorff.
In the Hausdorff uniformity, the powerset of a closed set is closed.
theorem
UniformSpace.hausdorff.isUniformEmbedding_singleton
{α : Type u_1}
[UniformSpace α]
:
IsUniformEmbedding fun (x : α) => {x}
theorem
UniformSpace.hausdorff.isClosedEmbedding_singleton
{α : Type u_1}
[UniformSpace α]
[T0Space α]
:
Topology.IsClosedEmbedding fun (x : α) => {x}
theorem
UniformSpace.hausdorff.uniformContinuous_union
{α : Type u_1}
[UniformSpace α]
:
UniformContinuous fun (x : Set α × Set α) => x.1 ∪ x.2
instance
UniformSpace.hausdorff.instDiscreteUniformitySet
{α : Type u_1}
[UniformSpace α]
[DiscreteUniformity α]
:
theorem
UniformContinuous.image_hausdorff
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : UniformContinuous f)
:
UniformContinuous fun (x : Set α) => f '' x
When Set is equipped with the Hausdorff uniformity, taking the image under a uniformly
continuous map is uniformly continuous.
theorem
IsUniformInducing.image_hausdorff
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
:
IsUniformInducing fun (x : Set α) => f '' x
When Set is equipped with the Hausdorff uniformity, taking the image under a uniform
inducing map is uniform inducing.
theorem
IsUniformEmbedding.image_hausdorff
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformEmbedding f)
:
IsUniformEmbedding fun (x : Set α) => f '' x
When Set is equipped with the Hausdorff uniformity, taking the image under a uniform
embedding is a uniform embedding.
theorem
TotallyBounded.powerset_hausdorff
{α : Type u_1}
[UniformSpace α]
{t : Set α}
(ht : TotallyBounded t)
:
TotallyBounded (𝒫 t)
In the Hausdorff uniformity, the powerset of a totally bounded set is totally bounded.
theorem
TotallyBounded.nhds_vietoris_le_nhds_hausdorff
{α : Type u_1}
[UniformSpace α]
{s : Set α}
(hs : TotallyBounded s)
:
The neighborhoods of a totally bounded set in the Hausdorff uniformity are neighborhoods in the Vietoris topology.
theorem
IsCompact.nhds_hausdorff_eq_nhds_vietoris
{α : Type u_1}
[UniformSpace α]
{s : Set α}
(hs : IsCompact s)
:
A compact set has the same neighborhoods in the Hausdorff uniformity and the Vietoris topology.
instance
UniformSpace.hausdorff.instCompactSpaceSet
{α : Type u_1}
[UniformSpace α]
[CompactSpace α]
:
CompactSpace (Set α)
instance
TopologicalSpace.Closeds.uniformSpace
{α : Type u_1}
[UniformSpace α]
:
UniformSpace (Closeds α)
Equations
theorem
Filter.HasBasis.uniformity_closeds
{α : Type u_1}
[UniformSpace α]
{ι : Sort u_3}
{p : ι → Prop}
{s : ι → Set (α × α)}
(h : (uniformity α).HasBasis p s)
:
(uniformity (TopologicalSpace.Closeds α)).HasBasis p fun (i : ι) =>
Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (s i)
theorem
TopologicalSpace.Closeds.totallyBounded_subsets_of_totallyBounded
{α : Type u_1}
[UniformSpace α]
{t : Set α}
(ht : TotallyBounded t)
:
instance
TopologicalSpace.Closeds.instDiscreteUniformity
{α : Type u_1}
[UniformSpace α]
[DiscreteUniformity α]
:
theorem
TopologicalSpace.Closeds.isUniformEmbedding_singleton
{α : Type u_1}
[UniformSpace α]
[T0Space α]
:
IsUniformEmbedding fun (x : α) => {x}
theorem
TopologicalSpace.Closeds.uniformContinuous_singleton
{α : Type u_1}
[UniformSpace α]
[T0Space α]
:
UniformContinuous fun (x : α) => {x}
theorem
TopologicalSpace.Closeds.isEmbedding_singleton
{α : Type u_1}
[UniformSpace α]
[T0Space α]
:
Topology.IsEmbedding fun (x : α) => {x}
theorem
TopologicalSpace.Closeds.continuous_singleton
{α : Type u_1}
[UniformSpace α]
[T0Space α]
:
Continuous fun (x : α) => {x}
theorem
TopologicalSpace.Closeds.isClosedEmbedding_singleton
{α : Type u_1}
[UniformSpace α]
[T0Space α]
:
Topology.IsClosedEmbedding fun (x : α) => {x}
@[simp]
theorem
TopologicalSpace.Closeds.discreteUniformity_iff
{α : Type u_1}
[UniformSpace α]
[T0Space α]
:
theorem
TopologicalSpace.Closeds.uniformContinuous_sup
{α : Type u_1}
[UniformSpace α]
:
UniformContinuous fun (x : Closeds α × Closeds α) => x.1 ⊔ x.2
theorem
UniformContinuous.sup_closeds
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f g : α → TopologicalSpace.Closeds β}
(hf : UniformContinuous f)
(hg : UniformContinuous g)
:
UniformContinuous fun (x : α) => f x ⊔ g x
instance
TopologicalSpace.Closeds.instContinuousSup
{α : Type u_1}
[UniformSpace α]
:
ContinuousSup (Closeds α)
instance
TopologicalSpace.Closeds.instCompactSpace
{α : Type u_1}
[UniformSpace α]
[CompactSpace α]
:
CompactSpace (Closeds α)
@[simp]
@[simp]
instance
TopologicalSpace.Closeds.instNoncompactSpace
{α : Type u_1}
[UniformSpace α]
[NoncompactSpace α]
:
instance
TopologicalSpace.Compacts.uniformSpace
{α : Type u_1}
[UniformSpace α]
:
UniformSpace (Compacts α)
Equations
theorem
Filter.HasBasis.uniformity_compacts
{α : Type u_1}
[UniformSpace α]
{ι : Sort u_3}
{p : ι → Prop}
{s : ι → Set (α × α)}
(h : (uniformity α).HasBasis p s)
:
(uniformity (TopologicalSpace.Compacts α)).HasBasis p fun (i : ι) =>
Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (s i)
theorem
TopologicalSpace.Compacts.isUniformEmbedding_toCloseds
{α : Type u_1}
[UniformSpace α]
[T2Space α]
:
theorem
TopologicalSpace.Compacts.uniformContinuous_toCloseds
{α : Type u_1}
[UniformSpace α]
[T2Space α]
:
theorem
TopologicalSpace.Compacts.isEmbedding_toCloseds
{α : Type u_1}
[UniformSpace α]
[T2Space α]
:
theorem
TopologicalSpace.Compacts.continuous_toCloseds
{α : Type u_1}
[UniformSpace α]
[T2Space α]
:
theorem
TopologicalSpace.Compacts.totallyBounded_subsets_of_totallyBounded
{α : Type u_1}
[UniformSpace α]
{t : Set α}
(ht : TotallyBounded t)
:
theorem
TopologicalSpace.Compacts.isUniformEmbedding_singleton
{α : Type u_1}
[UniformSpace α]
:
IsUniformEmbedding fun (x : α) => {x}
theorem
TopologicalSpace.Compacts.uniformContinuous_singleton
{α : Type u_1}
[UniformSpace α]
:
UniformContinuous fun (x : α) => {x}
theorem
TopologicalSpace.Compacts.uniformContinuous_sup
{α : Type u_1}
[UniformSpace α]
:
UniformContinuous fun (x : Compacts α × Compacts α) => x.1 ⊔ x.2
theorem
UniformContinuous.sup_compacts
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f g : α → TopologicalSpace.Compacts β}
(hf : UniformContinuous f)
(hg : UniformContinuous g)
:
UniformContinuous fun (x : α) => f x ⊔ g x
theorem
UniformContinuous.compacts_map
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : UniformContinuous f)
:
theorem
IsUniformInducing.compacts_map
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
:
theorem
IsUniformEmbedding.compacts_map
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformEmbedding f)
:
instance
TopologicalSpace.Compacts.instDiscreteUniformity
{α : Type u_1}
[UniformSpace α]
[DiscreteUniformity α]
:
@[simp]
Equations
theorem
Filter.HasBasis.uniformity_nonemptyCompacts
{α : Type u_1}
[UniformSpace α]
{ι : Sort u_3}
{p : ι → Prop}
{s : ι → Set (α × α)}
(h : (uniformity α).HasBasis p s)
:
(uniformity (TopologicalSpace.NonemptyCompacts α)).HasBasis p fun (i : ι) =>
Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (s i)
theorem
TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds
{α : Type u_1}
[UniformSpace α]
[T2Space α]
:
theorem
TopologicalSpace.NonemptyCompacts.uniformContinuous_toCloseds
{α : Type u_1}
[UniformSpace α]
[T2Space α]
:
theorem
TopologicalSpace.NonemptyCompacts.isEmbedding_toCloseds
{α : Type u_1}
[UniformSpace α]
[T2Space α]
:
theorem
TopologicalSpace.NonemptyCompacts.continuous_toCloseds
{α : Type u_1}
[UniformSpace α]
[T2Space α]
:
theorem
TopologicalSpace.NonemptyCompacts.totallyBounded_subsets_of_totallyBounded
{α : Type u_1}
[UniformSpace α]
{t : Set α}
(ht : TotallyBounded t)
:
TotallyBounded {K : NonemptyCompacts α | ↑K ⊆ t}
theorem
TopologicalSpace.NonemptyCompacts.isUniformEmbedding_singleton
{α : Type u_1}
[UniformSpace α]
:
IsUniformEmbedding fun (x : α) => {x}
theorem
TopologicalSpace.NonemptyCompacts.uniformContinuous_singleton
{α : Type u_1}
[UniformSpace α]
:
UniformContinuous fun (x : α) => {x}
theorem
TopologicalSpace.NonemptyCompacts.uniformContinuous_sup
{α : Type u_1}
[UniformSpace α]
:
UniformContinuous fun (x : NonemptyCompacts α × NonemptyCompacts α) => x.1 ⊔ x.2
theorem
UniformContinuous.sup_nonemptyCompacts
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f g : α → TopologicalSpace.NonemptyCompacts β}
(hf : UniformContinuous f)
(hg : UniformContinuous g)
:
UniformContinuous fun (x : α) => f x ⊔ g x
theorem
UniformContinuous.nonemptyCompacts_map
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : UniformContinuous f)
:
theorem
IsUniformInducing.nonemptyCompacts_map
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
:
theorem
IsUniformEmbedding.nonemptyCompacts_map
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformEmbedding f)
:
instance
TopologicalSpace.NonemptyCompacts.instDiscreteUniformity
{α : Type u_1}
[UniformSpace α]
[DiscreteUniformity α]
:
@[simp]