Dense embeddings #
This file defines three properties of functions:
DenseRange fmeansfhas dense image;IsDenseInducing imeansiis also inducing, namely it induces the topology on its codomain;IsDenseEmbedding emeanseis further an embedding, namely it is injective andInducing.
The main theorem continuous_extend gives a criterion for a function
f : X → Z to a T₃ space Z to extend along a dense embedding
i : X → Y to a continuous function g : Y → Z. Actually i only
has to be IsDenseInducing (not necessarily injective).
structure
IsDenseInducing
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(i : α → β)
extends Topology.IsInducing i :
i : α → β is "dense inducing" if it has dense range and the topology on α
is the one induced by i from the topology on β.
- dense : DenseRange i
The range of a dense inducing map is a dense set.
theorem
IsDenseInducing.isInducing
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : IsDenseInducing i)
:
theorem
IsDenseInducing.nhds_eq_comap
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : IsDenseInducing i)
(a : α)
:
theorem
IsDenseInducing.continuous
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : IsDenseInducing i)
:
theorem
IsDenseInducing.closure_range
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : IsDenseInducing i)
:
theorem
IsDenseInducing.preconnectedSpace
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[PreconnectedSpace α]
(di : IsDenseInducing i)
:
theorem
IsDenseInducing.closure_image_mem_nhds
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
{s : Set α}
{a : α}
(di : IsDenseInducing i)
(hs : s ∈ nhds a)
:
theorem
IsDenseInducing.dense_image
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : IsDenseInducing i)
{s : Set α}
:
theorem
IsDenseInducing.interior_compact_eq_empty
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[T2Space β]
(di : IsDenseInducing i)
(hd : Dense (Set.range i)ᶜ)
{s : Set α}
(hs : IsCompact s)
:
If i : α → β is a dense embedding with dense complement of the range, then any compact set in
α has empty interior.
theorem
IsDenseInducing.prodMap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{e₁ : α → β}
{e₂ : γ → δ}
(de₁ : IsDenseInducing e₁)
(de₂ : IsDenseInducing e₂)
:
IsDenseInducing (Prod.map e₁ e₂)
The product of two dense inducings is a dense inducing
@[deprecated IsDenseInducing.prodMap (since := "2024-10-06")]
theorem
IsDenseInducing.prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{e₁ : α → β}
{e₂ : γ → δ}
(de₁ : IsDenseInducing e₁)
(de₂ : IsDenseInducing e₂)
:
IsDenseInducing (Prod.map e₁ e₂)
Alias of IsDenseInducing.prodMap.
The product of two dense inducings is a dense inducing
theorem
IsDenseInducing.separableSpace
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace.SeparableSpace α]
(di : IsDenseInducing i)
:
If the domain of a IsDenseInducing map is a separable space, then so is the codomain.
theorem
IsDenseInducing.tendsto_comap_nhds_nhds
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace δ]
{f : γ → α}
{g : γ → δ}
{h : δ → β}
{d : δ}
{a : α}
(di : IsDenseInducing i)
(H : Filter.Tendsto h (nhds d) (nhds (i a)))
(comm : h ∘ g = i ∘ f)
:
Filter.Tendsto f (Filter.comap g (nhds d)) (nhds a)
γ -f→ α
g↓ ↓e
δ -h→ β
theorem
IsDenseInducing.nhdsWithin_neBot
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : IsDenseInducing i)
(b : β)
:
(nhdsWithin b (Set.range i)).NeBot
theorem
IsDenseInducing.comap_nhds_neBot
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : IsDenseInducing i)
(b : β)
:
(Filter.comap i (nhds b)).NeBot
def
IsDenseInducing.extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
(di : IsDenseInducing i)
(f : α → γ)
(b : β)
:
γ
If i : α → β is a dense inducing, then any function f : α → γ "extends" to a function g = IsDenseInducing.extend di f : β → γ. If γ is Hausdorff and f has a continuous extension, then
g is the unique such extension. In general, g might not be continuous or even extend f.
Equations
- di.extend f b = limUnder (Filter.comap i (nhds b)) f
theorem
IsDenseInducing.extend_eq_of_tendsto
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T2Space γ]
(di : IsDenseInducing i)
{b : β}
{c : γ}
{f : α → γ}
(hf : Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c))
:
theorem
IsDenseInducing.extend_eq_at
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T2Space γ]
(di : IsDenseInducing i)
{f : α → γ}
{a : α}
(hf : ContinuousAt f a)
:
theorem
IsDenseInducing.extend_eq_at'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T2Space γ]
(di : IsDenseInducing i)
{f : α → γ}
{a : α}
(c : γ)
(hf : Filter.Tendsto f (nhds a) (nhds c))
:
theorem
IsDenseInducing.extend_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T2Space γ]
(di : IsDenseInducing i)
{f : α → γ}
(hf : Continuous f)
(a : α)
:
theorem
IsDenseInducing.extend_eq'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T2Space γ]
{f : α → γ}
(di : IsDenseInducing i)
(hf : ∀ (b : β), ∃ (c : γ), Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c))
(a : α)
:
Variation of extend_eq where we ask that f has a limit along comap i (𝓝 b) for each
b : β. This is a strictly stronger assumption than continuity of f, but in a lot of cases
you'd have to prove it anyway to use continuous_extend, so this avoids doing the work twice.
theorem
IsDenseInducing.extend_unique_at
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T2Space γ]
{b : β}
{f : α → γ}
{g : β → γ}
(di : IsDenseInducing i)
(hf : ∀ᶠ (x : α) in Filter.comap i (nhds b), g (i x) = f x)
(hg : ContinuousAt g b)
:
theorem
IsDenseInducing.extend_unique
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T2Space γ]
{f : α → γ}
{g : β → γ}
(di : IsDenseInducing i)
(hf : ∀ (x : α), g (i x) = f x)
(hg : Continuous g)
:
theorem
IsDenseInducing.continuousAt_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T3Space γ]
{b : β}
{f : α → γ}
(di : IsDenseInducing i)
(hf : ∀ᶠ (x : β) in nhds b, ∃ (c : γ), Filter.Tendsto f (Filter.comap i (nhds x)) (nhds c))
:
ContinuousAt (di.extend f) b
theorem
IsDenseInducing.continuous_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T3Space γ]
{f : α → γ}
(di : IsDenseInducing i)
(hf : ∀ (b : β), ∃ (c : γ), Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c))
:
Continuous (di.extend f)
theorem
IsDenseInducing.mk'
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(i : α → β)
(c : Continuous i)
(dense : ∀ (x : β), x ∈ closure (Set.range i))
(H : ∀ (a : α), ∀ s ∈ nhds a, ∃ t ∈ nhds (i a), ∀ (b : α), i b ∈ t → b ∈ s)
:
noncomputable def
Dense.extend
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
(hs : Dense s)
(f : ↑s → β)
:
α → β
This is a shortcut for hs.isDenseInducing_val.extend f. It is useful because if s : Set α
is dense then the coercion (↑) : s → α automatically satisfies IsUniformInducing and
IsDenseInducing so this gives access to the theorems satisfied by a uniform extension by simply
mentioning the density hypothesis.
theorem
Dense.extend_eq_of_tendsto
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
{f : ↑s → β}
[T2Space β]
(hs : Dense s)
{a : α}
{b : β}
(hf : Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b))
:
theorem
Dense.extend_eq_at
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
[T2Space β]
(hs : Dense s)
{f : ↑s → β}
{x : ↑s}
(hf : ContinuousAt f x)
:
theorem
Dense.extend_eq
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
{f : ↑s → β}
[T2Space β]
(hs : Dense s)
(hf : Continuous f)
(x : ↑s)
:
theorem
Dense.extend_unique_at
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
{f : ↑s → β}
[T2Space β]
{a : α}
{g : α → β}
(hs : Dense s)
(hf : ∀ᶠ (x : ↑s) in Filter.comap Subtype.val (nhds a), g ↑x = f x)
(hg : ContinuousAt g a)
:
theorem
Dense.extend_unique
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
{f : ↑s → β}
[T2Space β]
{g : α → β}
(hs : Dense s)
(hf : ∀ (x : ↑s), g ↑x = f x)
(hg : Continuous g)
:
theorem
Dense.continuousAt_extend
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
{f : ↑s → β}
[T3Space β]
{a : α}
(hs : Dense s)
(hf : ∀ᶠ (x : α) in nhds a, ∃ (b : β), Filter.Tendsto f (Filter.comap Subtype.val (nhds x)) (nhds b))
:
ContinuousAt (hs.extend f) a
theorem
Dense.continuous_extend
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{s : Set α}
{f : ↑s → β}
[T3Space β]
(hs : Dense s)
(hf : ∀ (a : α), ∃ (b : β), Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b))
:
Continuous (hs.extend f)
structure
IsDenseEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(e : α → β)
extends IsDenseInducing e :
A dense embedding is an embedding with dense image.
- dense : DenseRange e
- injective : Function.Injective e
A dense embedding is injective.
theorem
IsDenseEmbedding.mk'
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(e : α → β)
(c : Continuous e)
(dense : DenseRange e)
(injective : Function.Injective e)
(H : ∀ (a : α), ∀ s ∈ nhds a, ∃ t ∈ nhds (e a), ∀ (b : α), e b ∈ t → b ∈ s)
:
theorem
IsDenseEmbedding.isDenseInducing
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
(de : IsDenseEmbedding e)
:
theorem
IsDenseEmbedding.inj_iff
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
(de : IsDenseEmbedding e)
{x y : α}
:
theorem
IsDenseEmbedding.isEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
(de : IsDenseEmbedding e)
:
@[deprecated IsDenseEmbedding.isEmbedding (since := "2024-10-26")]
theorem
IsDenseEmbedding.to_embedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
(de : IsDenseEmbedding e)
:
Alias of IsDenseEmbedding.isEmbedding.
theorem
IsDenseEmbedding.separableSpace
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
[TopologicalSpace.SeparableSpace α]
(de : IsDenseEmbedding e)
:
If the domain of a IsDenseEmbedding is a separable space, then so is its codomain.
theorem
IsDenseEmbedding.prodMap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{e₁ : α → β}
{e₂ : γ → δ}
(de₁ : IsDenseEmbedding e₁)
(de₂ : IsDenseEmbedding e₂)
:
IsDenseEmbedding fun (p : α × γ) => (e₁ p.1, e₂ p.2)
The product of two dense embeddings is a dense embedding.
@[deprecated IsDenseEmbedding.prodMap (since := "2024-10-06")]
theorem
IsDenseEmbedding.prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{e₁ : α → β}
{e₂ : γ → δ}
(de₁ : IsDenseEmbedding e₁)
(de₂ : IsDenseEmbedding e₂)
:
IsDenseEmbedding fun (p : α × γ) => (e₁ p.1, e₂ p.2)
Alias of IsDenseEmbedding.prodMap.
The product of two dense embeddings is a dense embedding.
@[simp]
theorem
IsDenseEmbedding.subtypeEmb_coe
{β : Type u_2}
[TopologicalSpace β]
{α : Type u_5}
(p : α → Prop)
(e : α → β)
(x : { x : α // p x })
:
theorem
IsDenseEmbedding.subtype
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
(de : IsDenseEmbedding e)
(p : α → Prop)
:
IsDenseEmbedding (subtypeEmb p e)
theorem
IsDenseEmbedding.dense_image
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
(de : IsDenseEmbedding e)
{s : Set α}
:
theorem
isClosed_property
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{e : α → β}
{p : β → Prop}
(he : DenseRange e)
(hp : IsClosed {x : β | p x})
(h : ∀ (a : α), p (e a))
(b : β)
:
p b
theorem
isClosed_property2
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{e : α → β}
{p : β → β → Prop}
(he : DenseRange e)
(hp : IsClosed {q : β × β | p q.1 q.2})
(h : ∀ (a₁ a₂ : α), p (e a₁) (e a₂))
(b₁ b₂ : β)
:
p b₁ b₂
theorem
isClosed_property3
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{e : α → β}
{p : β → β → β → Prop}
(he : DenseRange e)
(hp : IsClosed {q : β × β × β | p q.1 q.2.1 q.2.2})
(h : ∀ (a₁ a₂ a₃ : α), p (e a₁) (e a₂) (e a₃))
(b₁ b₂ b₃ : β)
:
p b₁ b₂ b₃
theorem
DenseRange.induction_on
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{e : α → β}
(he : DenseRange e)
{p : β → Prop}
(b₀ : β)
(hp : IsClosed {b : β | p b})
(ih : ∀ (a : α), p (e a))
:
p b₀
theorem
DenseRange.induction_on₂
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{e : α → β}
{p : β → β → Prop}
(he : DenseRange e)
(hp : IsClosed {q : β × β | p q.1 q.2})
(h : ∀ (a₁ a₂ : α), p (e a₁) (e a₂))
(b₁ b₂ : β)
:
p b₁ b₂
theorem
DenseRange.induction_on₃
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{e : α → β}
{p : β → β → β → Prop}
(he : DenseRange e)
(hp : IsClosed {q : β × β × β | p q.1 q.2.1 q.2.2})
(h : ∀ (a₁ a₂ a₃ : α), p (e a₁) (e a₂) (e a₃))
(b₁ b₂ b₃ : β)
:
p b₁ b₂ b₃
theorem
DenseRange.equalizer
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace β]
[TopologicalSpace γ]
[T2Space γ]
{f : α → β}
(hfd : DenseRange f)
{g h : β → γ}
(hg : Continuous g)
(hh : Continuous h)
(H : g ∘ f = h ∘ f)
:
Two continuous functions to a t2-space that agree on the dense range of a function are equal.
theorem
Filter.HasBasis.hasBasis_of_isDenseInducing
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[T3Space β]
{ι : Type u_5}
{s : ι → Set α}
{p : ι → Prop}
{x : α}
(h : (nhds x).HasBasis p s)
{f : α → β}
(hf : IsDenseInducing f)
: