Module docstring
{"# Uniform embeddings of uniform spaces.
Extension of uniform continuous functions. ","### Uniform inducing maps ","### Uniform embeddings "}
IsUniformInducing
structure
(f : α → β)
Full source
/-- A map `f : α → β` between uniform spaces is called *uniform inducing* if the uniformity filter
on `α` is the pullback of the uniformity filter on `β` under `Prod.map f f`. If `α` is a separated
space, then this implies that `f` is injective, hence it is a `IsUniformEmbedding`. -/
@[mk_iff]
structure IsUniformInducing (f : α → β) : Prop where
/-- The uniformity filter on the domain is the pullback of the uniformity filter on the codomain
under `Prod.map f f`. -/
comap_uniformity : comap (fun x : α × α => (f x.1, f x.2)) (𝓤 β) = 𝓤 αInformal description
A map \( f : \alpha \to \beta \) between uniform spaces is called *uniform inducing* if the uniformity filter on \( \alpha \) is the pullback of the uniformity filter on \( \beta \) under the product map \( \text{Prod.map } f \text{ } f \). If \( \alpha \) is a separated space, then this implies that \( f \) is injective.
isUniformInducing_iff_uniformSpace
theorem
{f : α → β} : IsUniformInducing f ↔ ‹UniformSpace β›.comap f = ‹UniformSpace α›
Full source
lemma isUniformInducing_iff_uniformSpace {f : α → β} :
IsUniformInducingIsUniformInducing f ↔ ‹UniformSpace β›.comap f = ‹UniformSpace α› := by
rw [isUniformInducing_iff, UniformSpace.ext_iff, Filter.ext_iff]
rflInformal description
A map $f \colon \alpha \to \beta$ between uniform spaces is uniform inducing if and only if the uniform space structure on $\alpha$ is equal to the pullback of the uniform space structure on $\beta$ along $f$. In other words, the uniformity on $\alpha$ is precisely the preimage of the uniformity on $\beta$ under the map $f \times f$.
isUniformInducing_iff'
theorem
{f : α → β} : IsUniformInducing f ↔ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
Full source
lemma isUniformInducing_iff' {f : α → β} :
IsUniformInducingIsUniformInducing f ↔ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α := by
rw [isUniformInducing_iff, UniformContinuous, tendsto_iff_comap, le_antisymm_iff, and_comm]; rflInformal description
A map $f \colon \alpha \to \beta$ between uniform spaces is uniform inducing if and only if $f$ is uniformly continuous and the pullback of the uniformity filter on $\beta$ under the product map $(f \times f)$ is finer than the uniformity filter on $\alpha$.
Filter.HasBasis.isUniformInducing_iff
theorem
{ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'} (h : (𝓤 α).HasBasis p s) (h' : (𝓤 β).HasBasis p' s') {f : α → β} :
IsUniformInducing f ↔
(∀ i, p' i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
(∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j)
Full source
protected lemma Filter.HasBasis.isUniformInducing_iff {ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'}
(h : (𝓤 α).HasBasis p s) (h' : (𝓤 β).HasBasis p' s') {f : α → β} :
IsUniformInducingIsUniformInducing f ↔
(∀ i, p' i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
(∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j) := by
simp [isUniformInducing_iff', h.uniformContinuous_iff h', (h'.comap _).le_basis_iff h, subset_def]Informal description
Let $\alpha$ and $\beta$ be uniform spaces with uniformity filters $\mathfrak{U}_\alpha$ and $\mathfrak{U}_\beta$ having bases indexed by $\iota$ and $\iota'$ respectively. Specifically, suppose $\mathfrak{U}_\alpha$ has a basis $\{s_j\}_{j \in \iota}$ where each $s_j$ satisfies property $p(j)$, and $\mathfrak{U}_\beta$ has a basis $\{s'_i\}_{i \in \iota'}$ where each $s'_i$ satisfies property $p'(i)$.
A map $f \colon \alpha \to \beta$ is uniform inducing if and only if:
1. For every $i \in \iota'$ with $p'(i)$, there exists $j \in \iota$ with $p(j)$ such that for all $x, y \in \alpha$, if $(x, y) \in s_j$ then $(f(x), f(y)) \in s'_i$.
2. For every $j \in \iota$ with $p(j)$, there exists $i \in \iota'$ with $p'(i)$ such that for all $x, y \in \alpha$, if $(f(x), f(y)) \in s'_i$ then $(x, y) \in s_j$.
IsUniformInducing.mk'
theorem
{f : α → β} (h : ∀ s, s ∈ 𝓤 α ↔ ∃ t ∈ 𝓤 β, ∀ x y : α, (f x, f y) ∈ t → (x, y) ∈ s) : IsUniformInducing f
Full source
theorem IsUniformInducing.mk' {f : α → β}
(h : ∀ s, s ∈ 𝓤 αs ∈ 𝓤 α ↔ ∃ t ∈ 𝓤 β, ∀ x y : α, (f x, f y) ∈ t → (x, y) ∈ s) : IsUniformInducing f :=
⟨by simp [eq_comm, Filter.ext_iff, subset_def, h]⟩Informal description
A map $f \colon \alpha \to \beta$ between uniform spaces is uniform inducing if for every set $s$ in the uniformity filter $\mathfrak{U}_\alpha$ of $\alpha$, there exists a set $t$ in the uniformity filter $\mathfrak{U}_\beta$ of $\beta$ such that for all $x, y \in \alpha$, if $(f(x), f(y)) \in t$ then $(x, y) \in s$, and conversely, for every such $t$ there exists such an $s$.
IsUniformInducing.id
theorem
: IsUniformInducing (@id α)
Full source
theorem IsUniformInducing.id : IsUniformInducing (@id α) :=
⟨by rw [← Prod.map_def, Prod.map_id, comap_id]⟩Informal description
The identity map $\text{id} : \alpha \to \alpha$ on a uniform space $\alpha$ is uniform inducing.
IsUniformInducing.comp
theorem
{g : β → γ} (hg : IsUniformInducing g) {f : α → β} (hf : IsUniformInducing f) : IsUniformInducing (g ∘ f)
Full source
theorem IsUniformInducing.comp {g : β → γ} (hg : IsUniformInducing g) {f : α → β}
(hf : IsUniformInducing f) : IsUniformInducing (g ∘ f) :=
⟨by rw [← hf.1, ← hg.1, comap_comap]; rfl⟩Informal description
Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be uniform inducing maps between uniform spaces. Then the composition $g \circ f : \alpha \to \gamma$ is also uniform inducing.
IsUniformInducing.of_comp_iff
theorem
{g : β → γ} (hg : IsUniformInducing g) {f : α → β} : IsUniformInducing (g ∘ f) ↔ IsUniformInducing f
Full source
theorem IsUniformInducing.of_comp_iff {g : β → γ} (hg : IsUniformInducing g) {f : α → β} :
IsUniformInducingIsUniformInducing (g ∘ f) ↔ IsUniformInducing f := by
refine ⟨fun h ↦ ?_, hg.comp⟩
rw [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, ← h.comap_uniformity,
Function.comp_def, Function.comp_def]Informal description
Let $g : \beta \to \gamma$ be a uniform inducing map between uniform spaces. For any map $f : \alpha \to \beta$, the composition $g \circ f$ is uniform inducing if and only if $f$ is uniform inducing.
IsUniformInducing.basis_uniformity
theorem
{f : α → β} (hf : IsUniformInducing f) {ι : Sort*} {p : ι → Prop} {s : ι → Set (β × β)} (H : (𝓤 β).HasBasis p s) :
(𝓤 α).HasBasis p fun i => Prod.map f f ⁻¹' s i
Full source
theorem IsUniformInducing.basis_uniformity {f : α → β} (hf : IsUniformInducing f) {ι : Sort*}
{p : ι → Prop} {s : ι → Set (β × β)} (H : (𝓤 β).HasBasis p s) :
(𝓤 α).HasBasis p fun i => Prod.mapProd.map f f ⁻¹' s i :=
hf.1 ▸ H.comap _Informal description
Let \( f : \alpha \to \beta \) be a uniform inducing map between uniform spaces. Suppose the uniformity filter \( \mathfrak{U}(\beta) \) on \( \beta \) has a basis consisting of sets \( s_i \subseteq \beta \times \beta \) indexed by \( i \in \iota \) with a predicate \( p \). Then the uniformity filter \( \mathfrak{U}(\alpha) \) on \( \alpha \) has a basis consisting of the preimages \( (\text{Prod.map } f \text{ } f)^{-1}(s_i) \) under the product map, indexed by the same \( i \in \iota \) with the same predicate \( p \).
IsUniformInducing.cauchy_map_iff
theorem
{f : α → β} (hf : IsUniformInducing f) {F : Filter α} : Cauchy (map f F) ↔ Cauchy F
Full source
theorem IsUniformInducing.cauchy_map_iff {f : α → β} (hf : IsUniformInducing f) {F : Filter α} :
CauchyCauchy (map f F) ↔ Cauchy F := by
simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap, ← hf.comap_uniformity]Informal description
Let \( f : \alpha \to \beta \) be a uniform inducing map between uniform spaces. For any filter \( F \) on \( \alpha \), the image filter \( f(F) \) is Cauchy if and only if \( F \) is Cauchy.
IsUniformInducing.of_comp
theorem
{f : α → β} {g : β → γ} (hf : UniformContinuous f) (hg : UniformContinuous g) (hgf : IsUniformInducing (g ∘ f)) :
IsUniformInducing f
Full source
theorem IsUniformInducing.of_comp {f : α → β} {g : β → γ} (hf : UniformContinuous f)
(hg : UniformContinuous g) (hgf : IsUniformInducing (g ∘ f)) : IsUniformInducing f := by
refine ⟨le_antisymm ?_ hf.le_comap⟩
rw [← hgf.1, ← Prod.map_def, ← Prod.map_def, ← Prod.map_comp_map f f g g, ← comap_comap]
exact comap_mono hg.le_comapInformal description
Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be uniformly continuous maps between uniform spaces. If the composition $g \circ f$ is a uniform inducing map, then $f$ is also a uniform inducing map.
IsUniformInducing.uniformContinuous
theorem
{f : α → β} (hf : IsUniformInducing f) : UniformContinuous f
Full source
theorem IsUniformInducing.uniformContinuous {f : α → β} (hf : IsUniformInducing f) :
UniformContinuous f := (isUniformInducing_iff'.1 hf).1Informal description
If a map $f \colon \alpha \to \beta$ between uniform spaces is uniform inducing, then $f$ is uniformly continuous.
IsUniformInducing.uniformContinuous_iff
theorem
{f : α → β} {g : β → γ} (hg : IsUniformInducing g) : UniformContinuous f ↔ UniformContinuous (g ∘ f)
Full source
theorem IsUniformInducing.uniformContinuous_iff {f : α → β} {g : β → γ} (hg : IsUniformInducing g) :
UniformContinuousUniformContinuous f ↔ UniformContinuous (g ∘ f) := by
dsimp only [UniformContinuous, Tendsto]
simp only [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, Function.comp_def]Informal description
Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be maps between uniform spaces. If $g$ is a uniform inducing map, then $f$ is uniformly continuous if and only if the composition $g \circ f$ is uniformly continuous.
IsUniformInducing.isUniformInducing_comp_iff
theorem
{f : α → β} {g : β → γ} (hg : IsUniformInducing g) : IsUniformInducing (g ∘ f) ↔ IsUniformInducing f
Full source
protected theorem IsUniformInducing.isUniformInducing_comp_iff {f : α → β} {g : β → γ}
(hg : IsUniformInducing g) : IsUniformInducingIsUniformInducing (g ∘ f) ↔ IsUniformInducing f := by
simp only [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, Function.comp_def]Informal description
Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be maps between uniform spaces. If $g$ is a uniform inducing map, then the composition $g \circ f$ is uniform inducing if and only if $f$ is uniform inducing.
IsUniformInducing.uniformContinuousOn_iff
theorem
{f : α → β} {g : β → γ} {S : Set α} (hg : IsUniformInducing g) :
UniformContinuousOn f S ↔ UniformContinuousOn (g ∘ f) S
Full source
theorem IsUniformInducing.uniformContinuousOn_iff {f : α → β} {g : β → γ} {S : Set α}
(hg : IsUniformInducing g) :
UniformContinuousOnUniformContinuousOn f S ↔ UniformContinuousOn (g ∘ f) S := by
dsimp only [UniformContinuousOn, Tendsto]
rw [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, comp_def, comp_def]Informal description
Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be maps between uniform spaces, and let $S \subseteq \alpha$ be a subset. If $g$ is a uniform inducing map, then $f$ is uniformly continuous on $S$ if and only if the composition $g \circ f$ is uniformly continuous on $S$.
IsUniformInducing.isInducing
theorem
{f : α → β} (h : IsUniformInducing f) : IsInducing f
Full source
theorem IsUniformInducing.isInducing {f : α → β} (h : IsUniformInducing f) : IsInducing f := by
obtain rfl := h.comap_uniformSpace
exact .induced fInformal description
If a map $f \colon \alpha \to \beta$ between uniform spaces is uniform inducing, then it is also inducing with respect to the induced topologies on $\alpha$ and $\beta$.
IsUniformInducing.prod
theorem
{α' : Type*} {β' : Type*} [UniformSpace α'] [UniformSpace β'] {e₁ : α → α'} {e₂ : β → β'} (h₁ : IsUniformInducing e₁)
(h₂ : IsUniformInducing e₂) : IsUniformInducing fun p : α × β => (e₁ p.1, e₂ p.2)
Full source
theorem IsUniformInducing.prod {α' : Type*} {β' : Type*} [UniformSpace α'] [UniformSpace β']
{e₁ : α → α'} {e₂ : β → β'} (h₁ : IsUniformInducing e₁) (h₂ : IsUniformInducing e₂) :
IsUniformInducing fun p : α × β => (e₁ p.1, e₂ p.2) :=
⟨by simp [Function.comp_def, uniformity_prod, ← h₁.1, ← h₂.1, comap_inf, comap_comap]⟩Informal description
Let $\alpha'$ and $\beta'$ be uniform spaces, and let $e_1 : \alpha \to \alpha'$ and $e_2 : \beta \to \beta'$ be uniform inducing maps. Then the product map $(e_1 \times e_2) : \alpha \times \beta \to \alpha' \times \beta'$ defined by $(x, y) \mapsto (e_1(x), e_2(y))$ is also uniform inducing.
IsUniformInducing.isDenseInducing
theorem
(h : IsUniformInducing f) (hd : DenseRange f) : IsDenseInducing f
Full source
lemma IsUniformInducing.isDenseInducing (h : IsUniformInducing f) (hd : DenseRange f) :
IsDenseInducing f where
toIsInducing := h.isInducing
dense := hdInformal description
Let $f \colon \alpha \to \beta$ be a uniform inducing map between uniform spaces. If $f$ has dense range, then $f$ is a dense inducing map with respect to the induced topologies on $\alpha$ and $\beta$.
SeparationQuotient.isUniformInducing_mk
theorem
: IsUniformInducing (mk : α → SeparationQuotient α)
Full source
lemma SeparationQuotient.isUniformInducing_mk :
IsUniformInducing (mk : α → SeparationQuotient α) :=
⟨comap_mk_uniformity⟩Informal description
The quotient map $\text{mk} \colon \alpha \to \text{SeparationQuotient}(\alpha)$ from a uniform space $\alpha$ to its separation quotient is uniform inducing. This means the uniformity on $\alpha$ is the pullback of the uniformity on $\text{SeparationQuotient}(\alpha)$ under the product map $\text{Prod.map mk mk}$.
IsUniformInducing.injective
theorem
[T0Space α] {f : α → β} (h : IsUniformInducing f) : Injective f
Full source
protected theorem IsUniformInducing.injective [T0Space α] {f : α → β} (h : IsUniformInducing f) :
Injective f :=
h.isInducing.injectiveInformal description
Let $\alpha$ be a T₀ space and $\beta$ a uniform space. If a map $f \colon \alpha \to \beta$ is uniform inducing, then $f$ is injective.
IsUniformEmbedding
structure
(f : α → β) : Prop extends IsUniformInducing f
Full source
/-- A map `f : α → β` between uniform spaces is a *uniform embedding* if it is uniform inducing and
injective. If `α` is a separated space, then the latter assumption follows from the former. -/
@[mk_iff]
structure IsUniformEmbedding (f : α → β) : Prop extends IsUniformInducing f where
/-- A uniform embedding is injective. -/
injective : Function.Injective fInformal description
A map $f : \alpha \to \beta$ between uniform spaces is called a *uniform embedding* if it is injective and uniformly continuous, and the uniformity on $\alpha$ is induced by $f$ from the uniformity on $\beta$ (i.e., the preimage of the uniformity on $\beta$ under the map $(f \times f)$ is contained in the uniformity on $\alpha$). If $\alpha$ is a separated space, then the injectivity condition follows from the uniform inducing property.
IsUniformEmbedding.isUniformInducing
theorem
(hf : IsUniformEmbedding f) : IsUniformInducing f
Full source
lemma IsUniformEmbedding.isUniformInducing (hf : IsUniformEmbedding f) : IsUniformInducing f :=
hf.toIsUniformInducingInformal description
If a map $f \colon \alpha \to \beta$ between uniform spaces is a uniform embedding, then it is also a uniform inducing map.
isUniformEmbedding_iff'
theorem
{f : α → β} : IsUniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
Informal description
A map $f \colon \alpha \to \beta$ between uniform spaces is a uniform embedding if and only if it is injective, uniformly continuous, and the pullback of the uniformity filter on $\beta$ under the product map $(f \times f)$ is finer than the uniformity filter on $\alpha$.
Filter.HasBasis.isUniformEmbedding_iff'
theorem
{ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'} (h : (𝓤 α).HasBasis p s) (h' : (𝓤 β).HasBasis p' s') {f : α → β} :
IsUniformEmbedding f ↔
Injective f ∧
(∀ i, p' i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
(∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j)
Full source
theorem Filter.HasBasis.isUniformEmbedding_iff' {ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'}
(h : (𝓤 α).HasBasis p s) (h' : (𝓤 β).HasBasis p' s') {f : α → β} :
IsUniformEmbeddingIsUniformEmbedding f ↔ Injective f ∧
(∀ i, p' i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
(∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j) := by
rw [isUniformEmbedding_iff, and_comm, h.isUniformInducing_iff h']Informal description
Let $\alpha$ and $\beta$ be uniform spaces with uniformity filters $\mathfrak{U}_\alpha$ and $\mathfrak{U}_\beta$ having bases $\{s_j\}_{j \in \iota}$ and $\{s'_i\}_{i \in \iota'}$ respectively, where each $s_j$ satisfies property $p(j)$ and each $s'_i$ satisfies property $p'(i)$.
A map $f \colon \alpha \to \beta$ is a uniform embedding if and only if:
1. $f$ is injective,
2. For every $i \in \iota'$ with $p'(i)$, there exists $j \in \iota$ with $p(j)$ such that for all $x, y \in \alpha$, $(x, y) \in s_j$ implies $(f(x), f(y)) \in s'_i$,
3. For every $j \in \iota$ with $p(j)$, there exists $i \in \iota'$ with $p'(i)$ such that for all $x, y \in \alpha$, $(f(x), f(y)) \in s'_i$ implies $(x, y) \in s_j$.
Filter.HasBasis.isUniformEmbedding_iff
theorem
{ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'} (h : (𝓤 α).HasBasis p s) (h' : (𝓤 β).HasBasis p' s') {f : α → β} :
IsUniformEmbedding f ↔
Injective f ∧ UniformContinuous f ∧ (∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j)
Full source
theorem Filter.HasBasis.isUniformEmbedding_iff {ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'}
(h : (𝓤 α).HasBasis p s) (h' : (𝓤 β).HasBasis p' s') {f : α → β} :
IsUniformEmbeddingIsUniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧
(∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j) := by
simp only [h.isUniformEmbedding_iff' h', h.uniformContinuous_iff h']Informal description
Let $\alpha$ and $\beta$ be uniform spaces with uniformity filters $\mathfrak{U}_\alpha$ and $\mathfrak{U}_\beta$ having bases $\{s_j\}_{j \in \iota}$ and $\{s'_i\}_{i \in \iota'}$ respectively, where each $s_j$ satisfies property $p(j)$ and each $s'_i$ satisfies property $p'(i)$.
A map $f \colon \alpha \to \beta$ is a uniform embedding if and only if:
1. $f$ is injective,
2. $f$ is uniformly continuous,
3. For every $j \in \iota$ with $p(j)$, there exists $i \in \iota'$ with $p'(i)$ such that for all $x, y \in \alpha$, $(f(x), f(y)) \in s'_i$ implies $(x, y) \in s_j$.
isUniformEmbedding_subtype_val
theorem
{p : α → Prop} : IsUniformEmbedding (Subtype.val : Subtype p → α)
Full source
theorem isUniformEmbedding_subtype_val {p : α → Prop} :
IsUniformEmbedding (Subtype.val : Subtype p → α) :=
{ comap_uniformity := rfl
injective := Subtype.val_injective }Informal description
For any subset of a uniform space $\alpha$ defined by a predicate $p : \alpha \to \text{Prop}$, the inclusion map $\text{Subtype.val} : \{x \in \alpha \mid p(x)\} \to \alpha$ is a uniform embedding.
isUniformEmbedding_set_inclusion
theorem
{s t : Set α} (hst : s ⊆ t) : IsUniformEmbedding (inclusion hst)
Full source
theorem isUniformEmbedding_set_inclusion {s t : Set α} (hst : s ⊆ t) :
IsUniformEmbedding (inclusion hst) where
comap_uniformity := by rw [uniformity_subtype, uniformity_subtype, comap_comap]; rfl
injective := inclusion_injective hstInformal description
For any subsets $s$ and $t$ of a uniform space $\alpha$ with $s \subseteq t$, the canonical inclusion map $\iota: s \hookrightarrow t$ is a uniform embedding. That is, $\iota$ is injective, uniformly continuous, and the uniformity on $s$ is induced by $\iota$ from the uniformity on $t$.
IsUniformEmbedding.comp
theorem
{g : β → γ} (hg : IsUniformEmbedding g) {f : α → β} (hf : IsUniformEmbedding f) : IsUniformEmbedding (g ∘ f)
Full source
theorem IsUniformEmbedding.comp {g : β → γ} (hg : IsUniformEmbedding g) {f : α → β}
(hf : IsUniformEmbedding f) : IsUniformEmbedding (g ∘ f) where
toIsUniformInducing := hg.isUniformInducing.comp hf.isUniformInducing
injective := hg.injective.comp hf.injectiveInformal description
Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be uniform embeddings between uniform spaces. Then the composition $g \circ f \colon \alpha \to \gamma$ is also a uniform embedding.
IsUniformEmbedding.of_comp_iff
theorem
{g : β → γ} (hg : IsUniformEmbedding g) {f : α → β} : IsUniformEmbedding (g ∘ f) ↔ IsUniformEmbedding f
Full source
theorem IsUniformEmbedding.of_comp_iff {g : β → γ} (hg : IsUniformEmbedding g) {f : α → β} :
IsUniformEmbeddingIsUniformEmbedding (g ∘ f) ↔ IsUniformEmbedding f := by
simp_rw [isUniformEmbedding_iff, hg.isUniformInducing.of_comp_iff, hg.injective.of_comp_iff f]Informal description
Let $g \colon \beta \to \gamma$ be a uniform embedding between uniform spaces. For any map $f \colon \alpha \to \beta$, the composition $g \circ f$ is a uniform embedding if and only if $f$ is a uniform embedding.
Equiv.isUniformEmbedding
theorem
{α β : Type*} [UniformSpace α] [UniformSpace β] (f : α ≃ β) (h₁ : UniformContinuous f)
(h₂ : UniformContinuous f.symm) : IsUniformEmbedding f
Full source
theorem Equiv.isUniformEmbedding {α β : Type*} [UniformSpace α] [UniformSpace β] (f : α ≃ β)
(h₁ : UniformContinuous f) (h₂ : UniformContinuous f.symm) : IsUniformEmbedding f :=
isUniformEmbedding_iff'.2 ⟨f.injective, h₁, by rwa [← Equiv.prodCongr_apply, ← map_equiv_symm]⟩Informal description
Let $\alpha$ and $\beta$ be uniform spaces, and let $f : \alpha \simeq \beta$ be an equivalence (bijection with inverse). If both $f$ and its inverse $f^{-1}$ are uniformly continuous, then $f$ is a uniform embedding.
isUniformEmbedding_inl
theorem
: IsUniformEmbedding (Sum.inl : α → α ⊕ β)
Full source
theorem isUniformEmbedding_inl : IsUniformEmbedding (Sum.inl : α → α ⊕ β) :=
isUniformEmbedding_iff'.2 ⟨Sum.inl_injective, uniformContinuous_inl, fun s hs =>
⟨Prod.map Sum.inl Sum.inl '' s ∪ range (Prod.map Sum.inr Sum.inr),
union_mem_sup (image_mem_map hs) range_mem_map,
fun x h => by simpa [Prod.map_apply'] using h⟩⟩Informal description
The left inclusion map $\text{inl} \colon \alpha \to \alpha \oplus \beta$ between uniform spaces is a uniform embedding. That is, $\text{inl}$ is injective, uniformly continuous, and the uniformity on $\alpha$ is induced by $\text{inl}$ from the uniformity on $\alpha \oplus \beta$.
isUniformEmbedding_inr
theorem
: IsUniformEmbedding (Sum.inr : β → α ⊕ β)
Full source
theorem isUniformEmbedding_inr : IsUniformEmbedding (Sum.inr : β → α ⊕ β) :=
isUniformEmbedding_iff'.2 ⟨Sum.inr_injective, uniformContinuous_inr, fun s hs =>
⟨range (Prod.map Sum.inl Sum.inl) ∪ Prod.map Sum.inr Sum.inr '' s,
union_mem_sup range_mem_map (image_mem_map hs),
fun x h => by simpa [Prod.map_apply'] using h⟩⟩Informal description
The right inclusion map $\operatorname{inr} : \beta \to \alpha \oplus \beta$ is a uniform embedding between uniform spaces $\beta$ and $\alpha \oplus \beta$.
IsUniformInducing.isUniformEmbedding
theorem
[T0Space α] {f : α → β} (hf : IsUniformInducing f) : IsUniformEmbedding f
Full source
/-- If the domain of a `IsUniformInducing` map `f` is a T₀ space, then `f` is injective,
hence it is a `IsUniformEmbedding`. -/
protected theorem IsUniformInducing.isUniformEmbedding [T0Space α] {f : α → β}
(hf : IsUniformInducing f) : IsUniformEmbedding f :=
⟨hf, hf.isInducing.injective⟩Informal description
Let $\alpha$ be a T₀ space and $\beta$ a uniform space. If a map $f \colon \alpha \to \beta$ is uniform inducing, then $f$ is a uniform embedding.
isUniformEmbedding_iff_isUniformInducing
theorem
[T0Space α] {f : α → β} : IsUniformEmbedding f ↔ IsUniformInducing f
Informal description
Let $\alpha$ be a T₀ space and $\beta$ a uniform space. A map $f \colon \alpha \to \beta$ is a uniform embedding if and only if it is a uniform inducing map.
comap_uniformity_of_spaced_out
theorem
{α} {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β) (hf : Pairwise fun x y => (f x, f y) ∉ s) :
comap (Prod.map f f) (𝓤 β) = 𝓟 idRel
Full source
/-- If a map `f : α → β` sends any two distinct points to point that are **not** related by a fixed
`s ∈ 𝓤 β`, then `f` is uniform inducing with respect to the discrete uniformity on `α`:
the preimage of `𝓤 β` under `Prod.map f f` is the principal filter generated by the diagonal in
`α × α`. -/
theorem comap_uniformity_of_spaced_out {α} {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β)
(hf : Pairwise fun x y => (f x, f y)(f x, f y) ∉ s) : comap (Prod.map f f) (𝓤 β) = 𝓟 idRel := by
refine le_antisymm ?_ (@refl_le_uniformity α (UniformSpace.comap f _))
calc
comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (𝓟 s) := comap_mono (le_principal_iff.2 hs)
_ = 𝓟 (Prod.mapProd.map f f ⁻¹' s) := comap_principal
_ ≤ 𝓟 idRel := principal_mono.2 ?_
rintro ⟨x, y⟩; simpa [not_imp_not] using @hf x yInformal description
Let $\alpha$ and $\beta$ be uniform spaces, and let $f : \alpha \to \beta$ be a map. Suppose there exists a set $s \in \mathcal{U}_\beta$ (the uniformity on $\beta$) such that for any two distinct points $x, y \in \alpha$, the pair $(f(x), f(y)) \notin s$. Then the preimage of the uniformity $\mathcal{U}_\beta$ under the map $\text{Prod.map } f \ f$ is equal to the principal filter generated by the diagonal relation $\text{idRel}$ on $\alpha \times \alpha$.
isUniformEmbedding_of_spaced_out
theorem
{α} {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β) (hf : Pairwise fun x y => (f x, f y) ∉ s) :
@IsUniformEmbedding α β ⊥ ‹_› f
Full source
/-- If a map `f : α → β` sends any two distinct points to point that are **not** related by a fixed
`s ∈ 𝓤 β`, then `f` is a uniform embedding with respect to the discrete uniformity on `α`. -/
theorem isUniformEmbedding_of_spaced_out {α} {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β)
(hf : Pairwise fun x y => (f x, f y)(f x, f y) ∉ s) : @IsUniformEmbedding α β ⊥ ‹_› f := by
let _ : UniformSpace α := ⊥; have := discreteTopology_bot α
exact IsUniformInducing.isUniformEmbedding ⟨comap_uniformity_of_spaced_out hs hf⟩Informal description
Let $\alpha$ and $\beta$ be uniform spaces, and let $f : \alpha \to \beta$ be a map. Suppose there exists a set $s \in \mathcal{U}_\beta$ (the uniformity on $\beta$) such that for any two distinct points $x, y \in \alpha$, the pair $(f(x), f(y)) \notin s$. Then $f$ is a uniform embedding when $\alpha$ is equipped with the discrete uniformity.
IsUniformEmbedding.isEmbedding
theorem
{f : α → β} (h : IsUniformEmbedding f) : IsEmbedding f
Full source
protected lemma IsUniformEmbedding.isEmbedding {f : α → β} (h : IsUniformEmbedding f) :
IsEmbedding f where
toIsInducing := h.toIsUniformInducing.isInducing
injective := h.injectiveInformal description
If a map $f \colon \alpha \to \beta$ between uniform spaces is a uniform embedding, then it is also a topological embedding (i.e., a homeomorphism onto its image).
IsUniformEmbedding.isDenseEmbedding
theorem
{f : α → β} (h : IsUniformEmbedding f) (hd : DenseRange f) : IsDenseEmbedding f
Full source
theorem IsUniformEmbedding.isDenseEmbedding {f : α → β} (h : IsUniformEmbedding f)
(hd : DenseRange f) : IsDenseEmbedding f :=
{ h.isEmbedding with dense := hd }Informal description
Let $f \colon \alpha \to \beta$ be a uniform embedding between uniform spaces. If $f$ has dense range (i.e., the image of $f$ is dense in $\beta$), then $f$ is a dense embedding (i.e., a topological embedding with dense image).
isClosedEmbedding_of_spaced_out
theorem
{α} [TopologicalSpace α] [DiscreteTopology α] [T0Space β] {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β)
(hf : Pairwise fun x y => (f x, f y) ∉ s) : IsClosedEmbedding f
Full source
theorem isClosedEmbedding_of_spaced_out {α} [TopologicalSpace α] [DiscreteTopology α]
[T0Space β] {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β)
(hf : Pairwise fun x y => (f x, f y)(f x, f y) ∉ s) : IsClosedEmbedding f := by
rcases @DiscreteTopology.eq_bot α _ _ with rfl; let _ : UniformSpace α := ⊥
exact
{ (isUniformEmbedding_of_spaced_out hs hf).isEmbedding with
isClosed_range := isClosed_range_of_spaced_out hs hf }Informal description
Let $\alpha$ be a topological space with the discrete topology, and let $\beta$ be a T₀ uniform space. Given a map $f \colon \alpha \to \beta$ and an entourage $s \in \mathcal{U}_\beta$ (the uniformity on $\beta$), if for every pair of distinct points $x, y \in \alpha$ the pair $(f(x), f(y)) \notin s$, then $f$ is a closed embedding (i.e., a topological embedding with closed image).
closure_image_mem_nhds_of_isUniformInducing
theorem
{s : Set (α × α)} {e : α → β} (b : β) (he₁ : IsUniformInducing e) (he₂ : IsDenseInducing e) (hs : s ∈ 𝓤 α) :
∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b
Full source
theorem closure_image_mem_nhds_of_isUniformInducing {s : Set (α × α)} {e : α → β} (b : β)
(he₁ : IsUniformInducing e) (he₂ : IsDenseInducing e) (hs : s ∈ 𝓤 α) :
∃ a, closure (e '' { a' | (a, a') ∈ s }) ∈ 𝓝 b := by
obtain ⟨U, ⟨hU, hUo, hsymm⟩, hs⟩ :
∃ U, (U ∈ 𝓤 β ∧ IsOpen U ∧ IsSymmetricRel U) ∧ Prod.map e e ⁻¹' U ⊆ s := by
rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs
rcases he₂.dense.mem_nhds (UniformSpace.ball_mem_nhds b hU) with ⟨a, ha⟩
refine ⟨a, mem_of_superset ?_ (closure_mono <| image_subset _ <| UniformSpace.ball_mono hs a)⟩
have ho : IsOpen (UniformSpace.ball (e a) U) := UniformSpace.isOpen_ball (e a) hUo
refine mem_of_superset (ho.mem_nhds <| (UniformSpace.mem_ball_symmetry hsymm).2 ha) fun y hy => ?_
refine mem_closure_iff_nhds.2 fun V hV => ?_
rcases he₂.dense.mem_nhds (inter_mem hV (ho.mem_nhds hy)) with ⟨x, hxV, hxU⟩
exact ⟨e x, hxV, mem_image_of_mem e hxU⟩Informal description
Let $\alpha$ and $\beta$ be uniform spaces, $e : \alpha \to \beta$ be a uniform inducing and dense inducing map, and $s \subseteq \alpha \times \alpha$ be an element of the uniformity on $\alpha$. Then for any point $b \in \beta$, there exists a point $a \in \alpha$ such that the closure of the image under $e$ of the set $\{a' \in \alpha \mid (a, a') \in s\}$ is a neighborhood of $b$ in $\beta$.
isUniformEmbedding_subtypeEmb
theorem
(p : α → Prop) {e : α → β} (ue : IsUniformEmbedding e) (de : IsDenseEmbedding e) :
IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e)
Full source
theorem isUniformEmbedding_subtypeEmb (p : α → Prop) {e : α → β} (ue : IsUniformEmbedding e)
(de : IsDenseEmbedding e) : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e) :=
{ comap_uniformity := by
simp [comap_comap, Function.comp_def, IsDenseEmbedding.subtypeEmb, uniformity_subtype,
ue.comap_uniformity.symm]
injective := (de.subtype p).injective }Informal description
Let $p : \alpha \to \text{Prop}$ be a predicate on $\alpha$, and let $e : \alpha \to \beta$ be a uniform embedding and dense embedding. Then the restriction of $e$ to the subtype defined by $p$, denoted as $\text{subtypeEmb}_p e$, is also a uniform embedding.
IsUniformEmbedding.prod
theorem
{α' : Type*} {β' : Type*} [UniformSpace α'] [UniformSpace β'] {e₁ : α → α'} {e₂ : β → β'} (h₁ : IsUniformEmbedding e₁)
(h₂ : IsUniformEmbedding e₂) : IsUniformEmbedding fun p : α × β => (e₁ p.1, e₂ p.2)
Full source
theorem IsUniformEmbedding.prod {α' : Type*} {β' : Type*} [UniformSpace α'] [UniformSpace β']
{e₁ : α → α'} {e₂ : β → β'} (h₁ : IsUniformEmbedding e₁) (h₂ : IsUniformEmbedding e₂) :
IsUniformEmbedding fun p : α × β => (e₁ p.1, e₂ p.2) where
toIsUniformInducing := h₁.isUniformInducing.prod h₂.isUniformInducing
injective := h₁.injective.prodMap h₂.injectiveInformal description
Let $\alpha'$ and $\beta'$ be uniform spaces, and let $e_1 \colon \alpha \to \alpha'$ and $e_2 \colon \beta \to \beta'$ be uniform embeddings. Then the product map $(e_1 \times e_2) \colon \alpha \times \beta \to \alpha' \times \beta'$ defined by $(x, y) \mapsto (e_1(x), e_2(y))$ is also a uniform embedding.
isComplete_image_iff
theorem
{m : α → β} {s : Set α} (hm : IsUniformInducing m) : IsComplete (m '' s) ↔ IsComplete s
Full source
/-- A set is complete iff its image under a uniform inducing map is complete. -/
theorem isComplete_image_iff {m : α → β} {s : Set α} (hm : IsUniformInducing m) :
IsCompleteIsComplete (m '' s) ↔ IsComplete s := by
have fact1 : SurjOn (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := surjOn_image .. |>.filter_map_Iic
have fact2 : MapsTo (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := mapsTo_image .. |>.filter_map_Iic
simp_rw [IsComplete, imp.swap (a := Cauchy _), ← mem_Iic (b := 𝓟 _), fact1.forall fact2,
hm.cauchy_map_iff, exists_mem_image, map_le_iff_le_comap, hm.isInducing.nhds_eq_comap]Informal description
Let $m \colon \alpha \to \beta$ be a uniform inducing map between uniform spaces, and let $s$ be a subset of $\alpha$. Then the image $m(s)$ is complete if and only if $s$ is complete.
IsUniformInducing.isComplete_iff
theorem
{f : α → β} {s : Set α} (hf : IsUniformInducing f) : IsComplete (f '' s) ↔ IsComplete s
Full source
/-- If `f : X → Y` is an `IsUniformInducing` map, the image `f '' s` of a set `s` is complete
if and only if `s` is complete. -/
theorem IsUniformInducing.isComplete_iff {f : α → β} {s : Set α} (hf : IsUniformInducing f) :
IsCompleteIsComplete (f '' s) ↔ IsComplete s := isComplete_image_iff hfInformal description
Let $f \colon \alpha \to \beta$ be a uniform inducing map between uniform spaces, and let $s$ be a subset of $\alpha$. Then the image $f(s)$ is complete if and only if $s$ is complete.
IsUniformEmbedding.isComplete_iff
theorem
{f : α → β} {s : Set α} (hf : IsUniformEmbedding f) : IsComplete (f '' s) ↔ IsComplete s
Full source
/-- If `f : X → Y` is an `IsUniformEmbedding`, the image `f '' s` of a set `s` is complete
if and only if `s` is complete. -/
theorem IsUniformEmbedding.isComplete_iff {f : α → β} {s : Set α} (hf : IsUniformEmbedding f) :
IsCompleteIsComplete (f '' s) ↔ IsComplete s := hf.isUniformInducing.isComplete_iffInformal description
Let $f \colon \alpha \to \beta$ be a uniform embedding between uniform spaces, and let $s$ be a subset of $\alpha$. Then the image $f(s)$ is complete if and only if $s$ is complete.
Subtype.isComplete_iff
theorem
{p : α → Prop} {s : Set { x // p x }} : IsComplete s ↔ IsComplete ((↑) '' s : Set α)
Full source
/-- Sets of a subtype are complete iff their image under the coercion is complete. -/
theorem Subtype.isComplete_iff {p : α → Prop} {s : Set { x // p x }} :
IsCompleteIsComplete s ↔ IsComplete ((↑) '' s : Set α) :=
isUniformEmbedding_subtype_val.isComplete_iff.symmInformal description
For any subset $s$ of a subtype $\{x \in \alpha \mid p(x)\}$ of a uniform space $\alpha$, the set $s$ is complete if and only if its image under the inclusion map $\iota : \{x \in \alpha \mid p(x)\} \to \alpha$ is a complete subset of $\alpha$.
completeSpace_iff_isComplete_range
theorem
{f : α → β} (hf : IsUniformInducing f) : CompleteSpace α ↔ IsComplete (range f)
Full source
theorem completeSpace_iff_isComplete_range {f : α → β} (hf : IsUniformInducing f) :
CompleteSpaceCompleteSpace α ↔ IsComplete (range f) := by
rw [completeSpace_iff_isComplete_univ, ← isComplete_image_iff hf, image_univ]Informal description
Let $f \colon \alpha \to \beta$ be a uniform inducing map between uniform spaces. Then the uniform space $\alpha$ is complete if and only if the range of $f$ is a complete subset of $\beta$.
IsUniformInducing.isComplete_range
theorem
[CompleteSpace α] (hf : IsUniformInducing f) : IsComplete (range f)
Full source
lemma IsUniformInducing.isComplete_range [CompleteSpace α] (hf : IsUniformInducing f) :
IsComplete (range f) :=
(completeSpace_iff_isComplete_range hf).1 ‹_›Informal description
Let $f \colon \alpha \to \beta$ be a uniform inducing map between uniform spaces. If $\alpha$ is a complete uniform space, then the range of $f$ is a complete subset of $\beta$.
IsUniformInducing.completeSpace_congr
theorem
{f : α → β} (hf : IsUniformInducing f) (hsurj : f.Surjective) : CompleteSpace α ↔ CompleteSpace β
Full source
/-- If `f` is a surjective uniform inducing map,
then its domain is a complete space iff its codomain is a complete space.
See also `_root_.completeSpace_congr` for a version that assumes `f` to be an equivalence. -/
theorem IsUniformInducing.completeSpace_congr {f : α → β} (hf : IsUniformInducing f)
(hsurj : f.Surjective) : CompleteSpaceCompleteSpace α ↔ CompleteSpace β := by
rw [completeSpace_iff_isComplete_range hf, hsurj.range_eq, completeSpace_iff_isComplete_univ]Informal description
Let $f \colon \alpha \to \beta$ be a surjective uniform inducing map between uniform spaces. Then $\alpha$ is a complete space if and only if $\beta$ is a complete space.
SeparationQuotient.completeSpace_iff
theorem
: CompleteSpace (SeparationQuotient α) ↔ CompleteSpace α
Informal description
The separation quotient of a uniform space $\alpha$ is complete if and only if $\alpha$ itself is complete.
SeparationQuotient.instCompleteSpace
instance
[CompleteSpace α] : CompleteSpace (SeparationQuotient α)
Full source
instance SeparationQuotient.instCompleteSpace [CompleteSpace α] :
CompleteSpace (SeparationQuotient α) :=
completeSpace_iff.2 ‹_›Informal description
For any complete uniform space $\alpha$, its separation quotient $\text{SeparationQuotient}(\alpha)$ is also a complete uniform space.
completeSpace_congr
theorem
{e : α ≃ β} (he : IsUniformEmbedding e) : CompleteSpace α ↔ CompleteSpace β
Full source
/-- See also `IsUniformInducing.completeSpace_congr`
for a version that works for non-injective maps. -/
theorem completeSpace_congr {e : α ≃ β} (he : IsUniformEmbedding e) :
CompleteSpaceCompleteSpace α ↔ CompleteSpace β :=
he.completeSpace_congr e.surjectiveInformal description
Let $e : \alpha \simeq \beta$ be a bijective uniform embedding between uniform spaces $\alpha$ and $\beta$. Then $\alpha$ is a complete space if and only if $\beta$ is a complete space.
completeSpace_coe_iff_isComplete
theorem
{s : Set α} : CompleteSpace s ↔ IsComplete s
Informal description
For any subset $s$ of a uniform space $\alpha$, the subspace $s$ is a complete uniform space if and only if $s$ is a complete subset of $\alpha$.
IsClosed.completeSpace_coe
theorem
[CompleteSpace α] {s : Set α} (hs : IsClosed s) : CompleteSpace s
Full source
theorem IsClosed.completeSpace_coe [CompleteSpace α] {s : Set α} (hs : IsClosed s) :
CompleteSpace s :=
hs.isComplete.completeSpace_coeInformal description
Let $\alpha$ be a complete uniform space and $s$ be a closed subset of $\alpha$. Then the subspace $s$ is also a complete uniform space.
completeSpace_ulift_iff
theorem
: CompleteSpace (ULift α) ↔ CompleteSpace α
Informal description
The uniform space $\mathrm{ULift}\,\alpha$ is complete if and only if the uniform space $\alpha$ is complete.
ULift.instCompleteSpace
instance
[CompleteSpace α] : CompleteSpace (ULift α)
Full source
/-- The lift of a complete space to another universe is still complete. -/
instance ULift.instCompleteSpace [CompleteSpace α] : CompleteSpace (ULift α) :=
completeSpace_ulift_iff.2 ‹_›Informal description
For any complete uniform space $\alpha$, the lifted space $\mathrm{ULift}\,\alpha$ is also complete.
completeSpace_extension
theorem
{m : β → α} (hm : IsUniformInducing m) (dense : DenseRange m) (h : ∀ f : Filter β, Cauchy f → ∃ x : α, map m f ≤ 𝓝 x) :
CompleteSpace α
Full source
theorem completeSpace_extension {m : β → α} (hm : IsUniformInducing m) (dense : DenseRange m)
(h : ∀ f : Filter β, Cauchy f → ∃ x : α, map m f ≤ 𝓝 x) : CompleteSpace α :=
⟨fun {f : Filter α} (hf : Cauchy f) =>
let p : Set (α × α) → Set α → Set α := fun s t => { y : α | ∃ x : α, x ∈ t ∧ (x, y) ∈ s }
let g := (𝓤 α).lift fun s => f.lift' (p s)
have mp₀ : Monotone p := fun _ _ h _ _ ⟨x, xs, xa⟩ => ⟨x, xs, h xa⟩
have mp₁ : ∀ {s}, Monotone (p s) := fun h _ ⟨y, ya, yxs⟩ => ⟨y, h ya, yxs⟩
have : f ≤ g := le_iInf₂ fun _ hs => le_iInf₂ fun _ ht =>
le_principal_iff.mpr <| mem_of_superset ht fun x hx => ⟨x, hx, refl_mem_uniformity hs⟩
have : NeBot g := hf.left.mono this
have : NeBot (comap m g) :=
comap_neBot fun _ ht =>
let ⟨t', ht', ht_mem⟩ := (mem_lift_sets <| monotone_lift' monotone_const mp₀).mp ht
let ⟨_, ht'', ht'_sub⟩ := (mem_lift'_sets mp₁).mp ht_mem
let ⟨x, hx⟩ := hf.left.nonempty_of_mem ht''
have h₀ : NeBot (𝓝[range m] x) := dense.nhdsWithin_neBot x
have h₁ : { y | (x, y) ∈ t' } ∈ 𝓝[range m] x :=
@mem_inf_of_left α (𝓝 x) (𝓟 (range m)) _ <| mem_nhds_left x ht'
have h₂ : range m ∈ 𝓝[range m] x :=
@mem_inf_of_right α (𝓝 x) (𝓟 (range m)) _ <| Subset.refl _
have : { y | (x, y) ∈ t' } ∩ range m ∈ 𝓝[range m] x := @inter_mem α (𝓝[range m] x) _ _ h₁ h₂
let ⟨_, xyt', b, b_eq⟩ := h₀.nonempty_of_mem this
⟨b, b_eq.symm ▸ ht'_sub ⟨x, hx, xyt'⟩⟩
have : Cauchy g :=
⟨‹NeBot g›, fun _ hs =>
let ⟨s₁, hs₁, comp_s₁⟩ := comp_mem_uniformity_sets hs
let ⟨s₂, hs₂, comp_s₂⟩ := comp_mem_uniformity_sets hs₁
let ⟨t, ht, (prod_t : t ×ˢ t ⊆ s₂)⟩ := mem_prod_same_iff.mp (hf.right hs₂)
have hg₁ : p (preimage Prod.swap s₁) t ∈ g :=
mem_lift (symm_le_uniformity hs₁) <| @mem_lift' α α f _ t ht
have hg₂ : p s₂ t ∈ g := mem_lift hs₂ <| @mem_lift' α α f _ t ht
have hg : p (Prod.swap ⁻¹' s₁) t ×ˢ p s₂ t ∈ g ×ˢ g := @prod_mem_prod α α _ _ g g hg₁ hg₂
(g ×ˢ g).sets_of_superset hg fun ⟨_, _⟩ ⟨⟨c₁, c₁t, hc₁⟩, ⟨c₂, c₂t, hc₂⟩⟩ =>
have : (c₁, c₂) ∈ t ×ˢ t := ⟨c₁t, c₂t⟩
comp_s₁ <| prodMk_mem_compRel hc₁ <| comp_s₂ <| prodMk_mem_compRel (prod_t this) hc₂⟩
have : Cauchy (Filter.comap m g) := ‹Cauchy g›.comap' (le_of_eq hm.comap_uniformity) ‹_›
let ⟨x, (hx : map m (Filter.comap m g) ≤ 𝓝 x)⟩ := h _ this
have : ClusterPt x (map m (Filter.comap m g)) :=
(le_nhds_iff_adhp_of_cauchy (this.map hm.uniformContinuous)).mp hx
have : ClusterPt x g := this.mono map_comap_le
⟨x,
calc
f ≤ g := by assumption
_ ≤ 𝓝 x := le_nhds_of_cauchy_adhp ‹Cauchy g› this
⟩⟩Informal description
Let $m \colon \beta \to \alpha$ be a uniform inducing map between uniform spaces with dense range. If for every Cauchy filter $\mathcal{F}$ on $\beta$, there exists a point $x \in \alpha$ such that the pushforward filter $m_*\mathcal{F}$ converges to $x$, then $\alpha$ is a complete uniform space.
totallyBounded_image_iff
theorem
{f : α → β} {s : Set α} (hf : IsUniformInducing f) : TotallyBounded (f '' s) ↔ TotallyBounded s
Full source
lemma totallyBounded_image_iff {f : α → β} {s : Set α} (hf : IsUniformInducing f) :
TotallyBoundedTotallyBounded (f '' s) ↔ TotallyBounded s := by
refine ⟨fun hs ↦ ?_, fun h ↦ h.image hf.uniformContinuous⟩
simp_rw [(hf.basis_uniformity (basis_sets _)).totallyBounded_iff]
intro t ht
rcases exists_subset_image_finite_and.1 (hs.exists_subset ht) with ⟨u, -, hfin, h⟩
use u, hfin
rwa [biUnion_image, image_subset_iff, preimage_iUnion₂] at hInformal description
Let \( f \colon \alpha \to \beta \) be a uniform inducing map between uniform spaces, and let \( s \subseteq \alpha \). Then the image \( f(s) \) is totally bounded in \( \beta \) if and only if \( s \) is totally bounded in \( \alpha \).
totallyBounded_preimage
theorem
{f : α → β} {s : Set β} (hf : IsUniformInducing f) (hs : TotallyBounded s) : TotallyBounded (f ⁻¹' s)
Full source
theorem totallyBounded_preimage {f : α → β} {s : Set β} (hf : IsUniformInducing f)
(hs : TotallyBounded s) : TotallyBounded (f ⁻¹' s) :=
(totallyBounded_image_iff hf).1 <| hs.subset <| image_preimage_subset ..Informal description
Let $f \colon \alpha \to \beta$ be a uniform inducing map between uniform spaces, and let $s \subseteq \beta$ be a totally bounded subset. Then the preimage $f^{-1}(s)$ is totally bounded in $\alpha$.
CompleteSpace.sum
instance
[CompleteSpace α] [CompleteSpace β] : CompleteSpace (α ⊕ β)
Full source
instance CompleteSpace.sum [CompleteSpace α] [CompleteSpace β] : CompleteSpace (α ⊕ β) := by
rw [completeSpace_iff_isComplete_univ, ← range_inl_union_range_inr]
exact isUniformEmbedding_inl.isUniformInducing.isComplete_range.union
isUniformEmbedding_inr.isUniformInducing.isComplete_rangeInformal description
For any two complete uniform spaces $\alpha$ and $\beta$, their direct sum $\alpha \oplus \beta$ is also a complete uniform space.
isUniformEmbedding_comap
theorem
{α : Type*} {β : Type*} {f : α → β} [u : UniformSpace β] (hf : Function.Injective f) :
@IsUniformEmbedding α β (UniformSpace.comap f u) u f
Full source
theorem isUniformEmbedding_comap {α : Type*} {β : Type*} {f : α → β} [u : UniformSpace β]
(hf : Function.Injective f) : @IsUniformEmbedding α β (UniformSpace.comap f u) u f :=
@IsUniformEmbedding.mk _ _ (UniformSpace.comap f u) _ _
(@IsUniformInducing.mk _ _ (UniformSpace.comap f u) _ _ rfl) hfInformal description
Let $\alpha$ and $\beta$ be types, with $\beta$ equipped with a uniform space structure. For an injective function $f : \alpha \to \beta$, the function $f$ is a uniform embedding when $\alpha$ is given the uniform space structure induced by $f$ (i.e., the coarsest uniformity making $f$ uniformly continuous).
Topology.IsEmbedding.comapUniformSpace
definition
{α β} [TopologicalSpace α] [u : UniformSpace β] (f : α → β) (h : IsEmbedding f) : UniformSpace α
Full source
/-- Pull back a uniform space structure by an embedding, adjusting the new uniform structure to
make sure that its topology is defeq to the original one. -/
def Topology.IsEmbedding.comapUniformSpace {α β} [TopologicalSpace α] [u : UniformSpace β]
(f : α → β) (h : IsEmbedding f) : UniformSpace α :=
(u.comap f).replaceTopology h.eq_inducedInformal description
Given topological spaces $\alpha$ and $\beta$, a uniform space structure on $\beta$, and an embedding $f : \alpha \to \beta$, this definition constructs a uniform space structure on $\alpha$ by pulling back the uniform structure from $\beta$ via $f$, while ensuring that the induced topology on $\alpha$ matches the original topology.
Embedding.to_isUniformEmbedding
theorem
{α β} [TopologicalSpace α] [u : UniformSpace β] (f : α → β) (h : IsEmbedding f) :
@IsUniformEmbedding α β (h.comapUniformSpace f) u f
Full source
theorem Embedding.to_isUniformEmbedding {α β} [TopologicalSpace α] [u : UniformSpace β] (f : α → β)
(h : IsEmbedding f) : @IsUniformEmbedding α β (h.comapUniformSpace f) u f :=
let _ := h.comapUniformSpace f
{ comap_uniformity := rfl
injective := h.injective }Informal description
Let $\alpha$ and $\beta$ be topological spaces, with $\beta$ equipped with a uniform space structure. Given an embedding $f : \alpha \to \beta$, the uniform space structure on $\alpha$ induced by $f$ via `IsEmbedding.comapUniformSpace` makes $f$ a uniform embedding. That is, $f$ is injective, uniformly continuous, and the uniformity on $\alpha$ is the pullback of the uniformity on $\beta$ under $f \times f$.
uniformly_extend_exists
theorem
[CompleteSpace γ] (a : α) : ∃ c, Tendsto f (comap e (𝓝 a)) (𝓝 c)
Full source
theorem uniformly_extend_exists [CompleteSpace γ] (a : α) : ∃ c, Tendsto f (comap e (𝓝 a)) (𝓝 c) :=
let de := h_e.isDenseInducing h_dense
have : Cauchy (𝓝 a) := cauchy_nhds
have : Cauchy (comap e (𝓝 a)) :=
this.comap' (le_of_eq h_e.comap_uniformity) (de.comap_nhds_neBot _)
have : Cauchy (map f (comap e (𝓝 a))) := this.map h_f
CompleteSpace.complete thisInformal description
Let $\alpha$, $\beta$, and $\gamma$ be uniform spaces with $\gamma$ complete. Given a map $e : \alpha \to \beta$ and a uniformly continuous map $f : \alpha \to \gamma$, for any point $a \in \alpha$, there exists a point $c \in \gamma$ such that $f$ tends to $c$ along the filter generated by pulling back neighborhoods of $a$ through $e$.
uniform_extend_subtype
theorem
[CompleteSpace γ] {p : α → Prop} {e : α → β} {f : α → γ} {b : β} {s : Set α}
(hf : UniformContinuous fun x : Subtype p => f x.val) (he : IsUniformEmbedding e)
(hd : ∀ x : β, x ∈ closure (range e)) (hb : closure (e '' s) ∈ 𝓝 b) (hs : IsClosed s) (hp : ∀ x ∈ s, p x) :
∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
Full source
theorem uniform_extend_subtype [CompleteSpace γ] {p : α → Prop} {e : α → β} {f : α → γ} {b : β}
{s : Set α} (hf : UniformContinuous fun x : Subtype p => f x.val) (he : IsUniformEmbedding e)
(hd : ∀ x : β, x ∈ closure (range e)) (hb : closureclosure (e '' s) ∈ 𝓝 b) (hs : IsClosed s)
(hp : ∀ x ∈ s, p x) : ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c) := by
have de : IsDenseEmbedding e := he.isDenseEmbedding hd
have de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e) := de.subtype p
have ue' : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e) :=
isUniformEmbedding_subtypeEmb _ he de
have : b ∈ closure (e '' { x | p x }) :=
(closure_mono <| monotone_image <| hp) (mem_of_mem_nhds hb)
let ⟨c, hc⟩ := uniformly_extend_exists ue'.isUniformInducing de'.dense hf ⟨b, this⟩
replace hc : Tendsto (f ∘ Subtype.val (p := p)) (((𝓝 b).comap e).comap Subtype.val) (𝓝 c) := by
simpa only [nhds_subtype_eq_comap, comap_comap, IsDenseEmbedding.subtypeEmb_coe] using hc
refine ⟨c, (tendsto_comap'_iff ?_).1 hc⟩
rw [Subtype.range_coe_subtype]
exact ⟨_, hb, by rwa [← de.isInducing.closure_eq_preimage_closure_image, hs.closure_eq]⟩Informal description
Let $\alpha$, $\beta$, and $\gamma$ be uniform spaces with $\gamma$ complete. Let $p : \alpha \to \mathrm{Prop}$ be a predicate on $\alpha$, $e : \alpha \to \beta$ be a uniform embedding, $f : \alpha \to \gamma$ be a function, $b \in \beta$, and $s \subseteq \alpha$ be a closed subset where $p$ holds for all $x \in s$. Suppose that:
1. The restriction of $f$ to the subtype $\{x \mid p x\}$ is uniformly continuous,
2. The range of $e$ is dense in $\beta$ (i.e., $\overline{\mathrm{range}(e)} = \beta$),
3. The closure of the image $e(s)$ is a neighborhood of $b$.
Then there exists a point $c \in \gamma$ such that $f$ tends to $c$ along the filter generated by pulling back neighborhoods of $b$ through $e$.
uniformly_extend_spec
theorem
[CompleteSpace γ] (a : α) : Tendsto f (comap e (𝓝 a)) (𝓝 (ψ a))
Full source
theorem uniformly_extend_spec [CompleteSpace γ] (a : α) : Tendsto f (comap e (𝓝 a)) (𝓝 (ψ a)) := by
simpa only [IsDenseInducing.extend] using
tendsto_nhds_limUnder (uniformly_extend_exists h_e ‹_› h_f _)Informal description
Let $\alpha$, $\beta$, and $\gamma$ be uniform spaces with $\gamma$ complete. Given a map $e : \alpha \to \beta$ and a uniformly continuous map $f : \alpha \to \gamma$, for any point $a \in \alpha$, the function $\psi$ satisfies that $f$ tends to $\psi(a)$ along the filter generated by pulling back neighborhoods of $a$ through $e$.
uniformContinuous_uniformly_extend
theorem
[CompleteSpace γ] : UniformContinuous ψ
Full source
theorem uniformContinuous_uniformly_extend [CompleteSpace γ] : UniformContinuous ψ := fun d hd =>
let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd
have h_pnt : ∀ {a m}, m ∈ 𝓝 a → ∃ c ∈ f '' (e ⁻¹' m), (c, ψ a) ∈ s ∧ (ψ a, c) ∈ s :=
fun {a m} hm =>
have nb : NeBot (map f (comap e (𝓝 a))) :=
((h_e.isDenseInducing h_dense).comap_nhds_neBot _).map _
have :
f '' (e ⁻¹' m)f '' (e ⁻¹' m) ∩ ({ c | (c, ψ a) ∈ s } ∩ { c | (ψ a, c) ∈ s })f '' (e ⁻¹' m) ∩ ({ c | (c, ψ a) ∈ s } ∩ { c | (ψ a, c) ∈ s }) ∈ map f (comap e (𝓝 a)) :=
inter_mem (image_mem_map <| preimage_mem_comap <| hm)
(uniformly_extend_spec h_e h_dense h_f _
(inter_mem (mem_nhds_right _ hs) (mem_nhds_left _ hs)))
nb.nonempty_of_mem this
have : (Prod.map f f) ⁻¹' s(Prod.map f f) ⁻¹' s ∈ 𝓤 β := h_f hs
have : (Prod.map f f) ⁻¹' s(Prod.map f f) ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α) := by
rwa [← h_e.comap_uniformity] at this
let ⟨t, ht, ts⟩ := this
show (Prod.map ψ ψ) ⁻¹' d(Prod.map ψ ψ) ⁻¹' d ∈ 𝓤 α from
mem_of_superset (interior_mem_uniformity ht) fun ⟨x₁, x₂⟩ hx_t => by
have : interiorinterior t ∈ 𝓝 (x₁, x₂) := isOpen_interior.mem_nhds hx_t
let ⟨m₁, hm₁, m₂, hm₂, (hm : m₁ ×ˢ m₂ ⊆ interior t)⟩ := mem_nhds_prod_iff.mp this
obtain ⟨_, ⟨a, ha₁, rfl⟩, _, ha₂⟩ := h_pnt hm₁
obtain ⟨_, ⟨b, hb₁, rfl⟩, hb₂, _⟩ := h_pnt hm₂
have : Prod.mapProd.map f f (a, b) ∈ s :=
ts <| mem_preimage.2 <| interior_subset (@hm (e a, e b) ⟨ha₁, hb₁⟩)
exact hs_comp ⟨f a, ha₂, ⟨f b, this, hb₂⟩⟩Informal description
Let $\alpha$, $\beta$, and $\gamma$ be uniform spaces with $\gamma$ complete. Given a uniformly continuous function $f : \alpha \to \gamma$ and a uniform embedding $e : \alpha \to \beta$, the extension $\psi : \beta \to \gamma$ is uniformly continuous.
uniformly_extend_of_ind
theorem
(b : β) : ψ (e b) = f b
Full source
theorem uniformly_extend_of_ind (b : β) : ψ (e b) = f b :=
IsDenseInducing.extend_eq_at _ h_f.continuous.continuousAtInformal description
For any point $b \in \beta$, the extended function $\psi$ evaluated at the image $e(b)$ equals the original function $f$ evaluated at $b$, i.e., $\psi(e(b)) = f(b)$.
uniformly_extend_unique
theorem
{g : α → γ} (hg : ∀ b, g (e b) = f b) (hc : Continuous g) : ψ = g
Full source
theorem uniformly_extend_unique {g : α → γ} (hg : ∀ b, g (e b) = f b) (hc : Continuous g) : ψ = g :=
IsDenseInducing.extend_unique _ hg hcInformal description
Let $\alpha$, $\beta$, and $\gamma$ be uniform spaces, with $e : \alpha \to \beta$ a uniform embedding and $f : \alpha \to \gamma$ a uniformly continuous function. Suppose $\psi : \beta \to \gamma$ is the uniform extension of $f$ along $e$. If $g : \beta \to \gamma$ is a continuous function such that $g(e(b)) = f(b)$ for all $b \in \beta$, then $\psi = g$.
isUniformInducing_val
theorem
(s : Set α) : IsUniformInducing (@Subtype.val α s)
Full source
theorem isUniformInducing_val (s : Set α) :
IsUniformInducing (@Subtype.val α s) := ⟨uniformity_setCoe⟩Informal description
For any subset $s$ of a uniform space $\alpha$, the inclusion map $\text{Subtype.val} : s \to \alpha$ is uniform inducing. This means the uniformity on $s$ is precisely the pullback of the uniformity on $\alpha$ under the map $(x, y) \mapsto (\text{val}(x), \text{val}(y))$.
Dense.extend_exists
theorem
[CompleteSpace β] (hs : Dense s) (hf : UniformContinuous f) (a : α) : ∃ b, Tendsto f (comap (↑) (𝓝 a)) (𝓝 b)
Full source
theorem extend_exists [CompleteSpace β] (hs : Dense s) (hf : UniformContinuous f) (a : α) :
∃ b, Tendsto f (comap (↑) (𝓝 a)) (𝓝 b) :=
uniformly_extend_exists (isUniformInducing_val s) hs.denseRange_val hf aInformal description
Let $\alpha$ and $\beta$ be uniform spaces with $\beta$ complete, and let $s$ be a dense subset of $\alpha$. Given a uniformly continuous function $f : s \to \beta$ and a point $a \in \alpha$, there exists a point $b \in \beta$ such that $f$ tends to $b$ along the filter generated by pulling back neighborhoods of $a$ through the inclusion map $(\uparrow) : s \to \alpha$.
Dense.extend_spec
theorem
[CompleteSpace β] (hs : Dense s) (hf : UniformContinuous f) (a : α) : Tendsto f (comap (↑) (𝓝 a)) (𝓝 (hs.extend f a))
Full source
theorem extend_spec [CompleteSpace β] (hs : Dense s) (hf : UniformContinuous f) (a : α) :
Tendsto f (comap (↑) (𝓝 a)) (𝓝 (hs.extend f a)) :=
uniformly_extend_spec (isUniformInducing_val s) hs.denseRange_val hf aInformal description
Let $\alpha$ and $\beta$ be uniform spaces with $\beta$ complete, and let $s$ be a dense subset of $\alpha$. Given a uniformly continuous function $f : s \to \beta$ and a point $a \in \alpha$, the function $f$ tends to the extended value $\text{hs.extend}\, f\, a$ along the filter generated by pulling back neighborhoods of $a$ through the inclusion map $(\uparrow) : s \to \alpha$.
Dense.uniformContinuous_extend
theorem
[CompleteSpace β] (hs : Dense s) (hf : UniformContinuous f) : UniformContinuous (hs.extend f)
Full source
theorem uniformContinuous_extend [CompleteSpace β] (hs : Dense s) (hf : UniformContinuous f) :
UniformContinuous (hs.extend f) :=
uniformContinuous_uniformly_extend (isUniformInducing_val s) hs.denseRange_val hfInformal description
Let $\alpha$ and $\beta$ be uniform spaces with $\beta$ complete, and let $s$ be a dense subset of $\alpha$. Given a uniformly continuous function $f : s \to \beta$, the extension $\text{hs.extend}\, f : \alpha \to \beta$ is uniformly continuous.
Dense.extend_of_ind
theorem
(hs : Dense s) (hf : UniformContinuous f) (x : s) : hs.extend f x = f x
Full source
theorem extend_of_ind (hs : Dense s) (hf : UniformContinuous f) (x : s) :
hs.extend f x = f x :=
IsDenseInducing.extend_eq_at _ hf.continuous.continuousAtInformal description
Let $s$ be a dense subset of a uniform space $\alpha$, and let $f : s \to \beta$ be a uniformly continuous function into a complete uniform space $\beta$. For any point $x \in s$, the extension of $f$ to $\alpha$ coincides with $f$ at $x$, i.e., $\text{hs.extend}\, f\, x = f x$.