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

@[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_2} {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 UniformSpace.hausdorff.isClosed_powerset {α : Type u_1} [UniformSpace α] {F : Set α} (hF : IsClosed F) :

IsClosed (𝒫 F)

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 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_2} {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 singleton

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

UniformContinuous singleton

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

Topology.IsEmbedding singleton

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

Continuous singleton

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

Topology.IsClosedEmbedding singleton

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_2} {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}

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_2} {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}