Uniform embeddings of uniform spaces. #
Extension of uniform continuous functions.
Uniform inducing maps #
structure
IsUniformInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
(f : α → β)
:
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.
The uniformity filter on the domain is the pullback of the uniformity filter on the codomain under
Prod.map f f.
Instances For
theorem
isUniformInducing_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
(f : α → β)
:
IsUniformInducing f ↔ Filter.comap (fun (x : α × α) => (f x.1, f x.2)) (uniformity β) = uniformity α
@[deprecated IsUniformInducing (since := "2024-10-08")]
Alias of IsUniformInducing.
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.
Equations
Instances For
theorem
isUniformInducing_iff_uniformSpace
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
@[deprecated isUniformInducing_iff_uniformSpace (since := "2024-10-05")]
theorem
uniformInducing_iff_uniformSpace
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
Alias of isUniformInducing_iff_uniformSpace.
theorem
IsUniformInducing.comap_uniformSpace
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
IsUniformInducing f → UniformSpace.comap f inst✝ = inst✝¹
Alias of the forward direction of isUniformInducing_iff_uniformSpace.
@[deprecated IsUniformInducing.comap_uniformSpace (since := "2024-10-08")]
theorem
UniformInducing.comap_uniformSpace
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
IsUniformInducing f → UniformSpace.comap f inst✝ = inst✝¹
Alias of the forward direction of isUniformInducing_iff_uniformSpace.
Alias of the forward direction of isUniformInducing_iff_uniformSpace.
theorem
isUniformInducing_iff'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
IsUniformInducing f ↔ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
@[deprecated isUniformInducing_iff' (since := "2024-10-05")]
theorem
uniformInducing_iff'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
IsUniformInducing f ↔ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
Alias of isUniformInducing_iff'.
theorem
Filter.HasBasis.isUniformInducing_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{ι : Sort u_1}
{ι' : Sort u_2}
{p : ι → Prop}
{p' : ι' → Prop}
{s : ι → Set (α × α)}
{s' : ι' → Set (β × β)}
(h : (uniformity α).HasBasis p s)
(h' : (uniformity β).HasBasis p' s')
{f : α → β}
:
@[deprecated Filter.HasBasis.isUniformInducing_iff (since := "2024-10-05")]
theorem
Filter.HasBasis.uniformInducing_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{ι : Sort u_1}
{ι' : Sort u_2}
{p : ι → Prop}
{p' : ι' → Prop}
{s : ι → Set (α × α)}
{s' : ι' → Set (β × β)}
(h : (uniformity α).HasBasis p s)
(h' : (uniformity β).HasBasis p' s')
{f : α → β}
:
Alias of Filter.HasBasis.isUniformInducing_iff.
theorem
IsUniformInducing.mk'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : ∀ (s : Set (α × α)), s ∈ uniformity α ↔ ∃ t ∈ uniformity β, ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s)
:
@[deprecated IsUniformInducing.mk' (since := "2024-10-05")]
theorem
UniformInducing.mk'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : ∀ (s : Set (α × α)), s ∈ uniformity α ↔ ∃ t ∈ uniformity β, ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s)
:
Alias of IsUniformInducing.mk'.
@[deprecated IsUniformInducing.id (since := "2024-10-05")]
Alias of IsUniformInducing.id.
theorem
IsUniformInducing.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformInducing g)
{f : α → β}
(hf : IsUniformInducing f)
:
IsUniformInducing (g ∘ f)
@[deprecated IsUniformInducing.comp (since := "2024-10-05")]
theorem
UniformInducing.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformInducing g)
{f : α → β}
(hf : IsUniformInducing f)
:
IsUniformInducing (g ∘ f)
Alias of IsUniformInducing.comp.
theorem
IsUniformInducing.of_comp_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformInducing g)
{f : α → β}
:
@[deprecated IsUniformInducing.of_comp_iff (since := "2024-10-05")]
theorem
UniformInducing.of_comp_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformInducing g)
{f : α → β}
:
Alias of IsUniformInducing.of_comp_iff.
theorem
IsUniformInducing.basis_uniformity
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
{ι : Sort u_1}
{p : ι → Prop}
{s : ι → Set (β × β)}
(H : (uniformity β).HasBasis p s)
:
(uniformity α).HasBasis p fun (i : ι) => Prod.map f f ⁻¹' s i
@[deprecated IsUniformInducing.basis_uniformity (since := "2024-10-05")]
theorem
UniformInducing.basis_uniformity
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
{ι : Sort u_1}
{p : ι → Prop}
{s : ι → Set (β × β)}
(H : (uniformity β).HasBasis p s)
:
(uniformity α).HasBasis p fun (i : ι) => Prod.map f f ⁻¹' s i
Alias of IsUniformInducing.basis_uniformity.
theorem
IsUniformInducing.cauchy_map_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
{F : Filter α}
:
@[deprecated IsUniformInducing.cauchy_map_iff (since := "2024-10-05")]
theorem
UniformInducing.cauchy_map_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
{F : Filter α}
:
Alias of IsUniformInducing.cauchy_map_iff.
theorem
IsUniformInducing.of_comp
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
(hf : UniformContinuous f)
(hg : UniformContinuous g)
(hgf : IsUniformInducing (g ∘ f))
:
@[deprecated IsUniformInducing.of_comp (since := "2024-10-05")]
theorem
uniformInducing_of_compose
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
(hf : UniformContinuous f)
(hg : UniformContinuous g)
(hgf : IsUniformInducing (g ∘ f))
:
Alias of IsUniformInducing.of_comp.
theorem
IsUniformInducing.uniformContinuous
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
:
@[deprecated IsUniformInducing.uniformContinuous (since := "2024-10-05")]
theorem
UniformInducing.uniformContinuous
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
:
Alias of IsUniformInducing.uniformContinuous.
theorem
IsUniformInducing.uniformContinuous_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
(hg : IsUniformInducing g)
:
@[deprecated IsUniformInducing.uniformContinuous_iff (since := "2024-10-05")]
theorem
UniformInducing.uniformContinuous_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
(hg : IsUniformInducing g)
:
Alias of IsUniformInducing.uniformContinuous_iff.
theorem
IsUniformInducing.isUniformInducing_comp_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
(hg : IsUniformInducing g)
:
@[deprecated IsUniformInducing.isUniformInducing_comp_iff (since := "2024-10-05")]
theorem
UniformInducing.uniformInducing_comp_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
(hg : IsUniformInducing g)
:
theorem
IsUniformInducing.uniformContinuousOn_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
{S : Set α}
(hg : IsUniformInducing g)
:
@[deprecated IsUniformInducing.uniformContinuousOn_iff (since := "2024-10-05")]
theorem
UniformInducing.uniformContinuousOn_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{f : α → β}
{g : β → γ}
{S : Set α}
(hg : IsUniformInducing g)
:
theorem
IsUniformInducing.isInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformInducing f)
:
@[deprecated IsUniformInducing.isInducing (since := "2024-10-28")]
theorem
IsUniformInducing.inducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformInducing f)
:
Alias of IsUniformInducing.isInducing.
@[deprecated IsUniformInducing.isInducing (since := "2024-10-05")]
theorem
UniformInducing.isInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformInducing f)
:
Alias of IsUniformInducing.isInducing.
@[deprecated UniformInducing.isInducing (since := "2024-10-28")]
theorem
UniformInducing.inducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformInducing f)
:
Alias of IsUniformInducing.isInducing.
Alias of IsUniformInducing.isInducing.
theorem
IsUniformInducing.prod
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{α' : Type u_1}
{β' : Type u_2}
[UniformSpace α']
[UniformSpace β']
{e₁ : α → α'}
{e₂ : β → β'}
(h₁ : IsUniformInducing e₁)
(h₂ : IsUniformInducing e₂)
:
IsUniformInducing fun (p : α × β) => (e₁ p.1, e₂ p.2)
@[deprecated IsUniformInducing.prod (since := "2024-10-05")]
theorem
UniformInducing.prod
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{α' : Type u_1}
{β' : Type u_2}
[UniformSpace α']
[UniformSpace β']
{e₁ : α → α'}
{e₂ : β → β'}
(h₁ : IsUniformInducing e₁)
(h₂ : IsUniformInducing e₂)
:
IsUniformInducing fun (p : α × β) => (e₁ p.1, e₂ p.2)
Alias of IsUniformInducing.prod.
theorem
IsUniformInducing.isDenseInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformInducing f)
(hd : DenseRange f)
:
@[deprecated IsUniformInducing.isDenseInducing (since := "2024-10-05")]
theorem
UniformInducing.isDenseInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformInducing f)
(hd : DenseRange f)
:
Alias of IsUniformInducing.isDenseInducing.
@[deprecated SeparationQuotient.isUniformInducing_mk (since := "2024-10-05")]
Alias of SeparationQuotient.isUniformInducing_mk.
theorem
IsUniformInducing.injective
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
(h : IsUniformInducing f)
:
@[deprecated IsUniformInducing.injective (since := "2024-10-05")]
theorem
UniformInducing.injective
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
(h : IsUniformInducing f)
:
Alias of IsUniformInducing.injective.
Uniform embeddings #
structure
IsUniformEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
(f : α → β)
extends IsUniformInducing f :
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.
- injective : Function.Injective f
A uniform embedding is injective.
Instances For
theorem
isUniformEmbedding_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
(f : α → β)
:
theorem
IsUniformEmbedding.isUniformInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformEmbedding f)
:
@[deprecated IsUniformEmbedding (since := "2024-10-03")]
Alias of IsUniformEmbedding.
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.
Equations
Instances For
theorem
isUniformEmbedding_iff'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
@[deprecated isUniformEmbedding_iff' (since := "2024-10-01")]
theorem
uniformEmbedding_iff'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
:
IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
Alias of isUniformEmbedding_iff'.
theorem
Filter.HasBasis.isUniformEmbedding_iff'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{ι : Sort u_1}
{ι' : Sort u_2}
{p : ι → Prop}
{p' : ι' → Prop}
{s : ι → Set (α × α)}
{s' : ι' → Set (β × β)}
(h : (uniformity α).HasBasis p s)
(h' : (uniformity β).HasBasis p' s')
{f : α → β}
:
@[deprecated Filter.HasBasis.isUniformEmbedding_iff' (since := "2024-10-01")]
theorem
Filter.HasBasis.uniformEmbedding_iff'
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{ι : Sort u_1}
{ι' : Sort u_2}
{p : ι → Prop}
{p' : ι' → Prop}
{s : ι → Set (α × α)}
{s' : ι' → Set (β × β)}
(h : (uniformity α).HasBasis p s)
(h' : (uniformity β).HasBasis p' s')
{f : α → β}
:
Alias of Filter.HasBasis.isUniformEmbedding_iff'.
theorem
Filter.HasBasis.isUniformEmbedding_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{ι : Sort u_1}
{ι' : Sort u_2}
{p : ι → Prop}
{p' : ι' → Prop}
{s : ι → Set (α × α)}
{s' : ι' → Set (β × β)}
(h : (uniformity α).HasBasis p s)
(h' : (uniformity β).HasBasis p' s')
{f : α → β}
:
IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ (j : ι), p j → ∃ (i : ι'), p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
@[deprecated Filter.HasBasis.isUniformEmbedding_iff (since := "2024-10-01")]
theorem
Filter.HasBasis.uniformEmbedding_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{ι : Sort u_1}
{ι' : Sort u_2}
{p : ι → Prop}
{p' : ι' → Prop}
{s : ι → Set (α × α)}
{s' : ι' → Set (β × β)}
(h : (uniformity α).HasBasis p s)
(h' : (uniformity β).HasBasis p' s')
{f : α → β}
:
IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ (j : ι), p j → ∃ (i : ι'), p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
Alias of Filter.HasBasis.isUniformEmbedding_iff.
@[deprecated isUniformEmbedding_subtype_val (since := "2024-10-01")]
Alias of isUniformEmbedding_subtype_val.
theorem
isUniformEmbedding_set_inclusion
{α : Type u}
[UniformSpace α]
{s t : Set α}
(hst : s ⊆ t)
:
@[deprecated isUniformEmbedding_set_inclusion (since := "2024-10-01")]
Alias of isUniformEmbedding_set_inclusion.
theorem
IsUniformEmbedding.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformEmbedding g)
{f : α → β}
(hf : IsUniformEmbedding f)
:
IsUniformEmbedding (g ∘ f)
@[deprecated IsUniformEmbedding.comp (since := "2024-10-01")]
theorem
UniformEmbedding.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformEmbedding g)
{f : α → β}
(hf : IsUniformEmbedding f)
:
IsUniformEmbedding (g ∘ f)
Alias of IsUniformEmbedding.comp.
theorem
IsUniformEmbedding.of_comp_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformEmbedding g)
{f : α → β}
:
@[deprecated IsUniformEmbedding.of_comp_iff (since := "2024-10-01")]
theorem
UniformEmbedding.of_comp_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{g : β → γ}
(hg : IsUniformEmbedding g)
{f : α → β}
:
Alias of IsUniformEmbedding.of_comp_iff.
theorem
Equiv.isUniformEmbedding
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
(f : α ≃ β)
(h₁ : UniformContinuous ⇑f)
(h₂ : UniformContinuous ⇑f.symm)
:
@[deprecated Equiv.isUniformEmbedding (since := "2024-10-01")]
theorem
Equiv.uniformEmbedding
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
(f : α ≃ β)
(h₁ : UniformContinuous ⇑f)
(h₂ : UniformContinuous ⇑f.symm)
:
Alias of Equiv.isUniformEmbedding.
@[deprecated isUniformEmbedding_inl (since := "2024-10-01")]
Alias of isUniformEmbedding_inl.
@[deprecated isUniformEmbedding_inr (since := "2024-10-01")]
Alias of isUniformEmbedding_inr.
theorem
IsUniformInducing.isUniformEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
(hf : IsUniformInducing f)
:
If the domain of a IsUniformInducing map f is a T₀ space, then f is injective,
hence it is a IsUniformEmbedding.
@[deprecated IsUniformInducing.isUniformEmbedding (since := "2024-10-05")]
theorem
UniformInducing.isUniformEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
(hf : IsUniformInducing f)
:
Alias of IsUniformInducing.isUniformEmbedding.
If the domain of a IsUniformInducing map f is a T₀ space, then f is injective,
hence it is a IsUniformEmbedding.
@[deprecated IsUniformInducing.isUniformEmbedding (since := "2024-10-01")]
theorem
IsUniformInducing.uniformEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
(hf : IsUniformInducing f)
:
Alias of IsUniformInducing.isUniformEmbedding.
If the domain of a IsUniformInducing map f is a T₀ space, then f is injective,
hence it is a IsUniformEmbedding.
theorem
isUniformEmbedding_iff_isUniformInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
:
@[deprecated isUniformEmbedding_iff_isUniformInducing (since := "2024-10-05")]
theorem
isUniformEmbedding_iff_uniformInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
:
Alias of isUniformEmbedding_iff_isUniformInducing.
@[deprecated isUniformEmbedding_iff_isUniformInducing (since := "2024-10-01")]
theorem
uniformEmbedding_iff_isUniformInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[T0Space α]
{f : α → β}
:
Alias of isUniformEmbedding_iff_isUniformInducing.
theorem
comap_uniformity_of_spaced_out
{β : Type v}
[UniformSpace β]
{α : Type u_1}
{f : α → β}
{s : Set (β × β)}
(hs : s ∈ uniformity β)
(hf : Pairwise fun (x y : α) => (f x, f y) ∉ s)
:
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
isUniformEmbedding_of_spaced_out
{β : Type v}
[UniformSpace β]
{α : Type u_1}
{f : α → β}
{s : Set (β × β)}
(hs : s ∈ uniformity β)
(hf : Pairwise fun (x y : α) => (f x, f y) ∉ s)
:
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 α.
@[deprecated isUniformEmbedding_of_spaced_out (since := "2024-10-01")]
theorem
uniformEmbedding_of_spaced_out
{β : Type v}
[UniformSpace β]
{α : Type u_1}
{f : α → β}
{s : Set (β × β)}
(hs : s ∈ uniformity β)
(hf : Pairwise fun (x y : α) => (f x, f y) ∉ s)
:
Alias of isUniformEmbedding_of_spaced_out.
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.isEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformEmbedding f)
:
@[deprecated IsUniformEmbedding.isEmbedding (since := "2024-10-26")]
theorem
IsUniformEmbedding.embedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformEmbedding f)
:
Alias of IsUniformEmbedding.isEmbedding.
@[deprecated IsUniformEmbedding.isEmbedding (since := "2024-10-01")]
theorem
UniformEmbedding.embedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformEmbedding f)
:
Alias of IsUniformEmbedding.isEmbedding.
theorem
IsUniformEmbedding.isDenseEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformEmbedding f)
(hd : DenseRange f)
:
@[deprecated IsUniformEmbedding.isDenseEmbedding (since := "2024-10-01")]
theorem
UniformEmbedding.isDenseEmbedding
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(h : IsUniformEmbedding f)
(hd : DenseRange f)
:
Alias of IsUniformEmbedding.isDenseEmbedding.
theorem
isClosedEmbedding_of_spaced_out
{β : Type v}
[UniformSpace β]
{α : Type u_1}
[TopologicalSpace α]
[DiscreteTopology α]
[T0Space β]
{f : α → β}
{s : Set (β × β)}
(hs : s ∈ uniformity β)
(hf : Pairwise fun (x y : α) => (f x, f y) ∉ s)
:
@[deprecated isClosedEmbedding_of_spaced_out (since := "2024-10-20")]
theorem
closedEmbedding_of_spaced_out
{β : Type v}
[UniformSpace β]
{α : Type u_1}
[TopologicalSpace α]
[DiscreteTopology α]
[T0Space β]
{f : α → β}
{s : Set (β × β)}
(hs : s ∈ uniformity β)
(hf : Pairwise fun (x y : α) => (f x, f y) ∉ s)
:
Alias of isClosedEmbedding_of_spaced_out.
theorem
closure_image_mem_nhds_of_isUniformInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{s : Set (α × α)}
{e : α → β}
(b : β)
(he₁ : IsUniformInducing e)
(he₂ : IsDenseInducing e)
(hs : s ∈ uniformity α)
:
@[deprecated closure_image_mem_nhds_of_isUniformInducing (since := "2024-10-05")]
theorem
closure_image_mem_nhds_of_uniformInducing
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{s : Set (α × α)}
{e : α → β}
(b : β)
(he₁ : IsUniformInducing e)
(he₂ : IsDenseInducing e)
(hs : s ∈ uniformity α)
:
theorem
isUniformEmbedding_subtypeEmb
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
(p : α → Prop)
{e : α → β}
(ue : IsUniformEmbedding e)
(de : IsDenseEmbedding e)
:
@[deprecated isUniformEmbedding_subtypeEmb (since := "2024-10-01")]
theorem
uniformEmbedding_subtypeEmb
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
(p : α → Prop)
{e : α → β}
(ue : IsUniformEmbedding e)
(de : IsDenseEmbedding e)
:
Alias of isUniformEmbedding_subtypeEmb.
theorem
IsUniformEmbedding.prod
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{α' : Type u_1}
{β' : Type u_2}
[UniformSpace α']
[UniformSpace β']
{e₁ : α → α'}
{e₂ : β → β'}
(h₁ : IsUniformEmbedding e₁)
(h₂ : IsUniformEmbedding e₂)
:
IsUniformEmbedding fun (p : α × β) => (e₁ p.1, e₂ p.2)
@[deprecated IsUniformEmbedding.prod (since := "2024-10-01")]
theorem
UniformEmbedding.prod
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{α' : Type u_1}
{β' : Type u_2}
[UniformSpace α']
[UniformSpace β']
{e₁ : α → α'}
{e₂ : β → β'}
(h₁ : IsUniformEmbedding e₁)
(h₂ : IsUniformEmbedding e₂)
:
IsUniformEmbedding fun (p : α × β) => (e₁ p.1, e₂ p.2)
Alias of IsUniformEmbedding.prod.
theorem
isComplete_image_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{m : α → β}
{s : Set α}
(hm : IsUniformInducing m)
:
A set is complete iff its image under a uniform inducing map is complete.
theorem
IsUniformInducing.isComplete_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set α}
(hf : IsUniformInducing f)
:
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.
@[deprecated IsUniformInducing.isComplete_iff (since := "2024-10-05")]
theorem
UniformInducing.isComplete_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set α}
(hf : IsUniformInducing f)
:
Alias of IsUniformInducing.isComplete_iff.
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
IsUniformEmbedding.isComplete_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set α}
(hf : IsUniformEmbedding f)
:
If f : X → Y is an IsUniformEmbedding, the image f '' s of a set s is complete
if and only if s is complete.
@[deprecated IsUniformEmbedding.isComplete_iff (since := "2024-10-01")]
theorem
UniformEmbedding.isComplete_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set α}
(hf : IsUniformEmbedding f)
:
Alias of IsUniformEmbedding.isComplete_iff.
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
Subtype.isComplete_iff
{α : Type u}
[UniformSpace α]
{p : α → Prop}
{s : Set { x : α // p x }}
:
Sets of a subtype are complete iff their image under the coercion is complete.
theorem
isComplete_of_complete_image
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{m : α → β}
{s : Set α}
(hm : IsUniformInducing m)
:
IsComplete (m '' s) → IsComplete s
Alias of the forward direction of isComplete_image_iff.
A set is complete iff its image under a uniform inducing map is complete.
theorem
completeSpace_iff_isComplete_range
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
:
theorem
IsUniformInducing.completeSpace
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
:
IsComplete (Set.range f) → CompleteSpace α
Alias of the reverse direction of completeSpace_iff_isComplete_range.
@[deprecated IsUniformInducing.completeSpace (since := "2024-10-08")]
theorem
UniformInducing.completeSpace
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
:
IsComplete (Set.range f) → CompleteSpace α
Alias of the reverse direction of completeSpace_iff_isComplete_range.
Alias of the reverse direction of completeSpace_iff_isComplete_range.
theorem
IsUniformInducing.isComplete_range
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
[CompleteSpace α]
(hf : IsUniformInducing f)
:
IsComplete (Set.range f)
@[deprecated IsUniformInducing.isComplete_range (since := "2024-10-05")]
theorem
UniformInducing.isComplete_range
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
[CompleteSpace α]
(hf : IsUniformInducing f)
:
IsComplete (Set.range f)
Alias of IsUniformInducing.isComplete_range.
theorem
IsUniformInducing.completeSpace_congr
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
(hsurj : Function.Surjective f)
:
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.
@[deprecated IsUniformInducing.completeSpace_congr (since := "2024-10-05")]
theorem
UniformInducing.completeSpace_congr
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
(hf : IsUniformInducing f)
(hsurj : Function.Surjective f)
:
Alias of IsUniformInducing.completeSpace_congr.
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
completeSpace_congr
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{e : α ≃ β}
(he : IsUniformEmbedding ⇑e)
:
See also IsUniformInducing.completeSpace_congr
for a version that works for non-injective maps.
theorem
IsComplete.completeSpace_coe
{α : Type u}
[UniformSpace α]
{s : Set α}
:
IsComplete s → CompleteSpace ↑s
Alias of the reverse direction of completeSpace_coe_iff_isComplete.
theorem
IsClosed.completeSpace_coe
{α : Type u}
[UniformSpace α]
[CompleteSpace α]
{s : Set α}
(hs : IsClosed s)
:
The lift of a complete space to another universe is still complete.
theorem
completeSpace_extension
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{m : β → α}
(hm : IsUniformInducing m)
(dense : DenseRange m)
(h : ∀ (f : Filter β), Cauchy f → ∃ (x : α), Filter.map m f ≤ nhds x)
:
theorem
totallyBounded_image_iff
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set α}
(hf : IsUniformInducing f)
:
theorem
totallyBounded_preimage
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
{f : α → β}
{s : Set β}
(hf : IsUniformInducing f)
(hs : TotallyBounded s)
:
TotallyBounded (f ⁻¹' s)
instance
CompleteSpace.sum
{α : Type u}
{β : Type v}
[UniformSpace α]
[UniformSpace β]
[CompleteSpace α]
[CompleteSpace β]
:
CompleteSpace (α ⊕ β)
theorem
isUniformEmbedding_comap
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[u : UniformSpace β]
(hf : Function.Injective f)
:
@[deprecated isUniformEmbedding_comap (since := "2024-10-01")]
theorem
uniformEmbedding_comap
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[u : UniformSpace β]
(hf : Function.Injective f)
:
Alias of isUniformEmbedding_comap.
def
Topology.IsEmbedding.comapUniformSpace
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[u : UniformSpace β]
(f : α → β)
(h : IsEmbedding f)
:
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.
Equations
Instances For
@[deprecated Topology.IsEmbedding.comapUniformSpace (since := "2024-10-26")]
def
Embedding.comapUniformSpace
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[u : UniformSpace β]
(f : α → β)
(h : Topology.IsEmbedding f)
:
Alias of Topology.IsEmbedding.comapUniformSpace.
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.
Instances For
theorem
Embedding.to_isUniformEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[u : UniformSpace β]
(f : α → β)
(h : Topology.IsEmbedding f)
:
@[deprecated Embedding.to_isUniformEmbedding (since := "2024-10-01")]
theorem
Embedding.to_uniformEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[u : UniformSpace β]
(f : α → β)
(h : Topology.IsEmbedding f)
:
Alias of Embedding.to_isUniformEmbedding.
theorem
uniformly_extend_exists
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{e : β → α}
(h_e : IsUniformInducing e)
(h_dense : DenseRange e)
{f : β → γ}
(h_f : UniformContinuous f)
[CompleteSpace γ]
(a : α)
:
∃ (c : γ), Filter.Tendsto f (Filter.comap e (nhds a)) (nhds c)
theorem
uniform_extend_subtype
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
[CompleteSpace γ]
{p : α → Prop}
{e : α → β}
{f : α → γ}
{b : β}
{s : Set α}
(hf : UniformContinuous fun (x : Subtype p) => f ↑x)
(he : IsUniformEmbedding e)
(hd : ∀ (x : β), x ∈ closure (Set.range e))
(hb : closure (e '' s) ∈ nhds b)
(hs : IsClosed s)
(hp : ∀ x ∈ s, p x)
:
∃ (c : γ), Filter.Tendsto f (Filter.comap e (nhds b)) (nhds c)
theorem
uniformly_extend_spec
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{e : β → α}
(h_e : IsUniformInducing e)
(h_dense : DenseRange e)
{f : β → γ}
(h_f : UniformContinuous f)
[CompleteSpace γ]
(a : α)
:
Filter.Tendsto f (Filter.comap e (nhds a)) (nhds (⋯.extend f a))
theorem
uniformContinuous_uniformly_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{e : β → α}
(h_e : IsUniformInducing e)
(h_dense : DenseRange e)
{f : β → γ}
(h_f : UniformContinuous f)
[CompleteSpace γ]
:
UniformContinuous (⋯.extend f)
theorem
uniformly_extend_of_ind
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{e : β → α}
(h_e : IsUniformInducing e)
(h_dense : DenseRange e)
{f : β → γ}
(h_f : UniformContinuous f)
[T0Space γ]
(b : β)
:
theorem
uniformly_extend_unique
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
{e : β → α}
(h_e : IsUniformInducing e)
(h_dense : DenseRange e)
{f : β → γ}
[T0Space γ]
{g : α → γ}
(hg : ∀ (b : β), g (e b) = f b)
(hc : Continuous g)
:
theorem
Dense.extend_exists
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{s : Set α}
{f : ↑s → β}
[CompleteSpace β]
(hs : Dense s)
(hf : UniformContinuous f)
(a : α)
:
∃ (b : β), Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b)
theorem
Dense.extend_spec
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{s : Set α}
{f : ↑s → β}
[CompleteSpace β]
(hs : Dense s)
(hf : UniformContinuous f)
(a : α)
:
Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds (hs.extend f a))
theorem
Dense.uniformContinuous_extend
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{s : Set α}
{f : ↑s → β}
[CompleteSpace β]
(hs : Dense s)
(hf : UniformContinuous f)
:
UniformContinuous (hs.extend f)
theorem
Dense.extend_of_ind
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
{s : Set α}
{f : ↑s → β}
[T0Space β]
(hs : Dense s)
(hf : UniformContinuous f)
(x : ↑s)
: