Documentation

Mathlib.Topology.UniformSpace.Closeds

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.

def hausdorffEntourage {α : Type u_1} (U : SetRel α α) :

SetRel (Set α) (Set α)

The set of pairs of sets contained in each other's thickening with respect to an entourage.

Equations

hausdorffEntourage U = {x : Set α × Set α | x.1 ⊆ U.preimage x.2 ∧ x.2 ⊆ U.image x.1}

Instances For

theorem mem_hausdorffEntourage {α : Type u_1} (U : SetRel α α) (s t : Set α) :

(s, t) ∈ hausdorffEntourage U ↔ s ⊆ U.preimage t ∧ t ⊆ U.image s

theorem hausdorffEntourage_mono {α : Type u_1} {U V : SetRel α α} (h : U ⊆ V) :

hausdorffEntourage U ⊆ hausdorffEntourage V

theorem monotone_hausdorffEntourage {α : Type u_1} :

Monotone hausdorffEntourage

instance isRefl_hausdorffEntourage {α : Type u_1} (U : SetRel α α) [U.IsRefl] :

(hausdorffEntourage U).IsRefl

@[simp]

theorem inv_hausdorffEntourage {α : Type u_1} (U : SetRel α α) :

(hausdorffEntourage U).inv = hausdorffEntourage U.inv

instance isSymm_hausdorffEntourage {α : Type u_1} (U : SetRel α α) [U.IsSymm] :

(hausdorffEntourage U).IsSymm

theorem hausdorffEntourage_comp {α : Type u_1} (U V : SetRel α α) :

hausdorffEntourage (U.comp V) = (hausdorffEntourage U).comp (hausdorffEntourage V)

instance isTrans_hausdorffEntourage {α : Type u_1} (U : SetRel α α) [U.IsTrans] :

(hausdorffEntourage U).IsTrans

@[simp]

theorem singleton_mem_hausdorffEntourage {α : Type u_1} (U : SetRel α α) (x y : α) :

({x}, {y}) ∈ hausdorffEntourage U ↔ (x, y) ∈ U

theorem union_mem_hausdorffEntourage {α : Type u_1} (U : SetRel α α) {s₁ s₂ t₁ t₂ : Set α} (h₁ : (s₁, t₁) ∈ hausdorffEntourage U) (h₂ : (s₂, t₂) ∈ hausdorffEntourage U) :

(s₁ ∪ s₂, t₁ ∪ t₂) ∈ hausdorffEntourage U

@[reducible, inline]

abbrev UniformSpace.hausdorff (α : Type u_1) [UniformSpace α] :

UniformSpace (Set α)

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

UniformSpace.hausdorff α = UniformSpace.ofCore { uniformity := (uniformity α).lift' hausdorffEntourage, refl := ⋯, symm := ⋯, comp := ⋯ }

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)

theorem UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen {α : Type u_1} [UniformSpace α] {U : Set α} (hU : IsOpen U) :

IsOpen {s : Set α | (s ∩ U).Nonempty}

theorem IsClosed.powerset_hausdorff {α : Type u_1} [UniformSpace α] {F : Set α} (hF : IsClosed F) :

IsClosed (𝒫 F)

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) :

IsClosed (𝒫 F)

Alias of IsClosed.powerset_hausdorff.

In the Hausdorff uniformity, the powerset of a closed set is closed.

theorem UniformSpace.hausdorff.isClopen_singleton_empty {α : Type u_1} [UniformSpace α] :

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

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.

instance TopologicalSpace.Closeds.uniformSpace {α : Type u_1} [UniformSpace α] :

UniformSpace (Closeds α)

Equations

TopologicalSpace.Closeds.uniformSpace = UniformSpace.comap SetLike.coe (UniformSpace.hausdorff α)

theorem TopologicalSpace.Closeds.uniformity_def {α : Type u_1} [UniformSpace α] :

uniformity (Closeds α) = Filter.comap (Prod.map SetLike.coe SetLike.coe) ((uniformity α).lift' hausdorffEntourage)

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.isUniformEmbedding_coe {α : Type u_1} [UniformSpace α] :

IsUniformEmbedding SetLike.coe

theorem TopologicalSpace.Closeds.uniformContinuous_coe {α : Type u_1} [UniformSpace α] :

UniformContinuous SetLike.coe

theorem TopologicalSpace.Closeds.isOpen_inter_nonempty_of_isOpen {α : Type u_1} [UniformSpace α] {s : Set α} (hs : IsOpen s) :

IsOpen {t : Closeds α | (↑t ∩ s).Nonempty}

theorem TopologicalSpace.Closeds.isClosed_subsets_of_isClosed {α : Type u_1} [UniformSpace α] {s : Set α} (hs : IsClosed s) :

IsClosed {t : Closeds α | ↑t ⊆ s}

theorem TopologicalSpace.Closeds.totallyBounded_subsets_of_totallyBounded {α : Type u_1} [UniformSpace α] {t : Set α} (ht : TotallyBounded t) :

TotallyBounded {F : Closeds α | ↑F ⊆ t}

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}

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.instT0Space {α : Type u_1} [UniformSpace α] :

T0Space (Closeds α)

instance TopologicalSpace.Compacts.uniformSpace {α : Type u_1} [UniformSpace α] :

UniformSpace (Compacts α)

Equations

TopologicalSpace.Compacts.uniformSpace = UniformSpace.comap SetLike.coe (UniformSpace.hausdorff α)

theorem TopologicalSpace.Compacts.uniformity_def {α : Type u_1} [UniformSpace α] :

uniformity (Compacts α) = Filter.comap (Prod.map SetLike.coe SetLike.coe) ((uniformity α).lift' hausdorffEntourage)

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_coe {α : Type u_1} [UniformSpace α] :

IsUniformEmbedding SetLike.coe

theorem TopologicalSpace.Compacts.uniformContinuous_coe {α : Type u_1} [UniformSpace α] :

UniformContinuous SetLike.coe

theorem TopologicalSpace.Compacts.isUniformEmbedding_toCloseds {α : Type u_1} [UniformSpace α] [T2Space α] :

IsUniformEmbedding toCloseds

theorem TopologicalSpace.Compacts.uniformContinuous_toCloseds {α : Type u_1} [UniformSpace α] [T2Space α] :

UniformContinuous toCloseds

theorem TopologicalSpace.Compacts.isEmbedding_toCloseds {α : Type u_1} [UniformSpace α] [T2Space α] :

Topology.IsEmbedding toCloseds

theorem TopologicalSpace.Compacts.continuous_toCloseds {α : Type u_1} [UniformSpace α] [T2Space α] :

Continuous toCloseds

theorem TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen {α : Type u_1} [UniformSpace α] {s : Set α} (hs : IsOpen s) :

IsOpen {t : Compacts α | (↑t ∩ s).Nonempty}

theorem TopologicalSpace.Compacts.isClosed_subsets_of_isClosed {α : Type u_1} [UniformSpace α] {s : Set α} (hs : IsClosed s) :

IsClosed {t : Compacts α | ↑t ⊆ s}

theorem TopologicalSpace.Compacts.totallyBounded_subsets_of_totallyBounded {α : Type u_1} [UniformSpace α] {t : Set α} (ht : TotallyBounded t) :

TotallyBounded {K : Compacts α | ↑K ⊆ 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) :

UniformContinuous (TopologicalSpace.Compacts.map f ⋯)

theorem IsUniformInducing.compacts_map {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {f : α → β} (hf : IsUniformInducing f) :

IsUniformInducing (TopologicalSpace.Compacts.map f ⋯)

theorem IsUniformEmbedding.compacts_map {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {f : α → β} (hf : IsUniformEmbedding f) :

IsUniformEmbedding (TopologicalSpace.Compacts.map f ⋯)

instance TopologicalSpace.NonemptyCompacts.uniformSpace {α : Type u_1} [UniformSpace α] :

UniformSpace (NonemptyCompacts α)

Equations

TopologicalSpace.NonemptyCompacts.uniformSpace = UniformSpace.comap SetLike.coe (UniformSpace.hausdorff α)

theorem TopologicalSpace.NonemptyCompacts.uniformity_def {α : Type u_1} [UniformSpace α] :

uniformity (NonemptyCompacts α) = Filter.comap (Prod.map SetLike.coe SetLike.coe) ((uniformity α).lift' hausdorffEntourage)

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_coe {α : Type u_1} [UniformSpace α] :

IsUniformEmbedding SetLike.coe

theorem TopologicalSpace.NonemptyCompacts.uniformContinuous_coe {α : Type u_1} [UniformSpace α] :

UniformContinuous SetLike.coe

theorem TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds {α : Type u_1} [UniformSpace α] [T2Space α] :

IsUniformEmbedding toCloseds

theorem TopologicalSpace.NonemptyCompacts.uniformContinuous_toCloseds {α : Type u_1} [UniformSpace α] [T2Space α] :

UniformContinuous toCloseds

theorem TopologicalSpace.NonemptyCompacts.isEmbedding_toCloseds {α : Type u_1} [UniformSpace α] [T2Space α] :

Topology.IsEmbedding toCloseds

theorem TopologicalSpace.NonemptyCompacts.continuous_toCloseds {α : Type u_1} [UniformSpace α] [T2Space α] :

Continuous toCloseds

theorem TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCompacts {α : Type u_1} [UniformSpace α] :

IsUniformEmbedding toCompacts

theorem TopologicalSpace.NonemptyCompacts.uniformContinuous_toCompacts {α : Type u_1} [UniformSpace α] :

UniformContinuous toCompacts

theorem TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts {α : Type u_1} [UniformSpace α] :

Topology.IsEmbedding toCompacts

theorem TopologicalSpace.NonemptyCompacts.continuous_toCompacts {α : Type u_1} [UniformSpace α] :

Continuous toCompacts

theorem TopologicalSpace.NonemptyCompacts.isOpen_inter_nonempty_of_isOpen {α : Type u_1} [UniformSpace α] {s : Set α} (hs : IsOpen s) :

IsOpen {t : NonemptyCompacts α | (↑t ∩ s).Nonempty}

theorem TopologicalSpace.NonemptyCompacts.isClosed_subsets_of_isClosed {α : Type u_1} [UniformSpace α] {s : Set α} (hs : IsClosed s) :

IsClosed {t : NonemptyCompacts α | ↑t ⊆ s}

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) :

UniformContinuous (TopologicalSpace.NonemptyCompacts.map f ⋯)

theorem IsUniformInducing.nonemptyCompacts_map {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {f : α → β} (hf : IsUniformInducing f) :

IsUniformInducing (TopologicalSpace.NonemptyCompacts.map f ⋯)

theorem IsUniformEmbedding.nonemptyCompacts_map {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {f : α → β} (hf : IsUniformEmbedding f) :

IsUniformEmbedding (TopologicalSpace.NonemptyCompacts.map f ⋯)