Dense embeddings #
This file defines three properties of functions:
DenseRange fmeansfhas dense image;DenseInducing imeansiis alsoInducing, namely it induces the topology on its codomain;DenseEmbedding emeanseis further anEmbedding, 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 DenseInducing (not necessarily injective).
structure
DenseInducing
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(i : α → β)
extends
Inducing
:
- induced : inst✝¹ = TopologicalSpace.induced i inst✝
- dense : DenseRange i
The range of a dense inducing map is a dense set.
i : α → β is "dense inducing" if it has dense range and the topology on α
is the one induced by i from the topology on β.
Instances For
theorem
DenseInducing.nhds_eq_comap
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : DenseInducing i)
(a : α)
:
nhds a = Filter.comap i (nhds (i a))
theorem
DenseInducing.continuous
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : DenseInducing i)
:
theorem
DenseInducing.closure_range
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : DenseInducing i)
:
theorem
DenseInducing.preconnectedSpace
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[PreconnectedSpace α]
(di : DenseInducing i)
:
theorem
DenseInducing.closure_image_mem_nhds
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
{s : Set α}
{a : α}
(di : DenseInducing i)
(hs : s ∈ nhds a)
:
theorem
DenseInducing.dense_image
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : DenseInducing i)
{s : Set α}
:
theorem
DenseInducing.interior_compact_eq_empty
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[T2Space β]
(di : DenseInducing 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
DenseInducing.prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{e₁ : α → β}
{e₂ : γ → δ}
(de₁ : DenseInducing e₁)
(de₂ : DenseInducing e₂)
:
DenseInducing fun p => (e₁ p.fst, e₂ p.snd)
The product of two dense inducings is a dense inducing
theorem
DenseInducing.separableSpace
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : DenseInducing i)
[TopologicalSpace.SeparableSpace α]
:
If the domain of a DenseInducing map is a separable space, then so is the codomain.
theorem
DenseInducing.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 : DenseInducing 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
DenseInducing.nhdsWithin_neBot
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : DenseInducing i)
(b : β)
:
Filter.NeBot (nhdsWithin b (Set.range i))
theorem
DenseInducing.comap_nhds_neBot
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : DenseInducing i)
(b : β)
:
Filter.NeBot (Filter.comap i (nhds b))
def
DenseInducing.extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
(di : DenseInducing i)
(f : α → γ)
(b : β)
:
γ
If i : α → β is a dense inducing, then any function f : α → γ "extends" to a function g = DenseInducing.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
- DenseInducing.extend di f b = limUnder (Filter.comap i (nhds b)) f
Instances For
theorem
DenseInducing.extend_eq_of_tendsto
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : DenseInducing i)
[TopologicalSpace γ]
[T2Space γ]
{b : β}
{c : γ}
{f : α → γ}
(hf : Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c))
:
DenseInducing.extend di f b = c
theorem
DenseInducing.extend_eq_at
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : DenseInducing i)
[TopologicalSpace γ]
[T2Space γ]
{f : α → γ}
{a : α}
(hf : ContinuousAt f a)
:
DenseInducing.extend di f (i a) = f a
theorem
DenseInducing.extend_eq_at'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : DenseInducing i)
[TopologicalSpace γ]
[T2Space γ]
{f : α → γ}
{a : α}
(c : γ)
(hf : Filter.Tendsto f (nhds a) (nhds c))
:
DenseInducing.extend di f (i a) = f a
theorem
DenseInducing.extend_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
(di : DenseInducing i)
[TopologicalSpace γ]
[T2Space γ]
{f : α → γ}
(hf : Continuous f)
(a : α)
:
DenseInducing.extend di f (i a) = f a
theorem
DenseInducing.extend_eq'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T2Space γ]
{f : α → γ}
(di : DenseInducing i)
(hf : ∀ (b : β), ∃ c, Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c))
(a : α)
:
DenseInducing.extend di f (i a) = f 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
DenseInducing.extend_unique_at
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T2Space γ]
{b : β}
{f : α → γ}
{g : β → γ}
(di : DenseInducing i)
(hf : ∀ᶠ (x : α) in Filter.comap i (nhds b), g (i x) = f x)
(hg : ContinuousAt g b)
:
DenseInducing.extend di f b = g b
theorem
DenseInducing.extend_unique
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T2Space γ]
{f : α → γ}
{g : β → γ}
(di : DenseInducing i)
(hf : ∀ (x : α), g (i x) = f x)
(hg : Continuous g)
:
DenseInducing.extend di f = g
theorem
DenseInducing.continuousAt_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T3Space γ]
{b : β}
{f : α → γ}
(di : DenseInducing i)
(hf : ∀ᶠ (x : β) in nhds b, ∃ c, Filter.Tendsto f (Filter.comap i (nhds x)) (nhds c))
:
ContinuousAt (DenseInducing.extend di f) b
theorem
DenseInducing.continuous_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[TopologicalSpace β]
{i : α → β}
[TopologicalSpace γ]
[T3Space γ]
{f : α → γ}
(di : DenseInducing i)
(hf : ∀ (b : β), ∃ c, Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c))
:
Continuous (DenseInducing.extend di f)
theorem
DenseInducing.mk'
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(i : α → β)
(c : Continuous i)
(dense : ∀ (x : β), x ∈ closure (Set.range i))
(H : ∀ (a : α) (s : Set α), s ∈ nhds a → ∃ t, t ∈ nhds (i a) ∧ ∀ (b : α), i b ∈ t → b ∈ s)
:
structure
DenseEmbedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(e : α → β)
extends
DenseInducing
:
- induced : inst✝¹ = TopologicalSpace.induced e inst✝
- dense : DenseRange e
- inj : Function.Injective e
A dense embedding is injective.
A dense embedding is an embedding with dense image.
Instances For
theorem
DenseEmbedding.mk'
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
(e : α → β)
(c : Continuous e)
(dense : DenseRange e)
(inj : Function.Injective e)
(H : ∀ (a : α) (s : Set α), s ∈ nhds a → ∃ t, t ∈ nhds (e a) ∧ ∀ (b : α), e b ∈ t → b ∈ s)
:
theorem
DenseEmbedding.inj_iff
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
(de : DenseEmbedding e)
{x : α}
{y : α}
:
theorem
DenseEmbedding.to_embedding
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
(de : DenseEmbedding e)
:
theorem
DenseEmbedding.separableSpace
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
(de : DenseEmbedding e)
[TopologicalSpace.SeparableSpace α]
:
If the domain of a DenseEmbedding is a separable space, then so is its codomain.
theorem
DenseEmbedding.prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[TopologicalSpace α]
[TopologicalSpace β]
[TopologicalSpace γ]
[TopologicalSpace δ]
{e₁ : α → β}
{e₂ : γ → δ}
(de₁ : DenseEmbedding e₁)
(de₂ : DenseEmbedding e₂)
:
DenseEmbedding fun p => (e₁ p.fst, e₂ p.snd)
The product of two dense embeddings is a dense embedding.
@[simp]
theorem
DenseEmbedding.subtypeEmb_coe
{β : Type u_2}
[TopologicalSpace β]
{α : Type u_5}
(p : α → Prop)
(e : α → β)
(x : { x // p x })
:
↑(DenseEmbedding.subtypeEmb p e x) = e ↑x
def
DenseEmbedding.subtypeEmb
{β : Type u_2}
[TopologicalSpace β]
{α : Type u_5}
(p : α → Prop)
(e : α → β)
(x : { x // p x })
:
The dense embedding of a subtype inside its closure.
Equations
- DenseEmbedding.subtypeEmb p e x = { val := e ↑x, property := (_ : e ↑x ∈ closure (e '' {x | p x})) }
Instances For
theorem
DenseEmbedding.subtype
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
(de : DenseEmbedding e)
(p : α → Prop)
:
theorem
DenseEmbedding.dense_image
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{e : α → β}
(de : DenseEmbedding e)
{s : Set α}
:
theorem
Dense.denseEmbedding_val
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
(hs : Dense s)
:
DenseEmbedding Subtype.val
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.fst q.snd})
(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.fst q.snd.fst q.snd.snd})
(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.fst q.snd})
(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.fst q.snd.fst q.snd.snd})
(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)
:
g = h
Two continuous functions to a t2-space that agree on the dense range of a function are equal.
theorem
Filter.HasBasis.hasBasis_of_denseInducing
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
[T3Space β]
{ι : Type u_5}
{s : ι → Set α}
{p : ι → Prop}
{x : α}
(h : Filter.HasBasis (nhds x) p s)
{f : α → β}
(hf : DenseInducing f)
:
Filter.HasBasis (nhds (f x)) p fun i => closure (f '' s i)