Dense embeddings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines three properties of functions:
dense_range fmeansfhas dense image;dense_inducing imeansiis alsoinducing, namely it induces the topology on its codomain;dense_embedding 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 dense_inducing (not necessarily injective).
structure
dense_inducing
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(i : α → β) :
Prop
- to_inducing : inducing i
- dense : dense_range i
i : α → β is "dense inducing" if it has dense range and the topology on α
is the one induced by i from the topology on β.
theorem
dense_inducing.nhds_eq_comap
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β}
(di : dense_inducing i)
(a : α) :
nhds a = filter.comap i (nhds (i a))
@[protected]
theorem
dense_inducing.continuous
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β}
(di : dense_inducing i) :
theorem
dense_inducing.closure_range
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β}
(di : dense_inducing i) :
@[protected]
theorem
dense_inducing.preconnected_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β}
[preconnected_space α]
(di : dense_inducing i) :
theorem
dense_inducing.closure_image_mem_nhds
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β}
{s : set α}
{a : α}
(di : dense_inducing i)
(hs : s ∈ nhds a) :
theorem
dense_inducing.dense_image
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β}
(di : dense_inducing i)
{s : set α} :
theorem
dense_inducing.interior_compact_eq_empty
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β}
[t2_space β]
(di : dense_inducing i)
(hd : dense (set.range i)ᶜ)
{s : set α}
(hs : is_compact s) :
If i : α → β is a dense embedding with dense complement of the range, then any compact set in
α has empty interior.
@[protected]
theorem
dense_inducing.prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{e₁ : α → β}
{e₂ : γ → δ}
(de₁ : dense_inducing e₁)
(de₂ : dense_inducing e₂) :
dense_inducing (λ (p : α × γ), (e₁ p.fst, e₂ p.snd))
The product of two dense inducings is a dense inducing
@[protected]
theorem
dense_inducing.separable_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β}
(di : dense_inducing i)
[topological_space.separable_space α] :
If the domain of a dense_inducing map is a separable space, then so is the codomain.
theorem
dense_inducing.tendsto_comap_nhds_nhds
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[topological_space β]
{i : α → β}
[topological_space δ]
{f : γ → α}
{g : γ → δ}
{h : δ → β}
{d : δ}
{a : α}
(di : dense_inducing 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→ β
@[protected]
theorem
dense_inducing.nhds_within_ne_bot
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β}
(di : dense_inducing i)
(b : β) :
(nhds_within b (set.range i)).ne_bot
theorem
dense_inducing.comap_nhds_ne_bot
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β}
(di : dense_inducing i)
(b : β) :
(filter.comap i (nhds b)).ne_bot
noncomputable
def
dense_inducing.extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
{i : α → β}
[topological_space γ]
(di : dense_inducing i)
(f : α → γ)
(b : β) :
γ
If i : α → β is a dense inducing, then any function f : α → γ "extends"
to a function g = 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 = lim (filter.comap i (nhds b)) f
theorem
dense_inducing.extend_eq_of_tendsto
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
{i : α → β}
(di : dense_inducing i)
[topological_space γ]
[t2_space γ]
{b : β}
{c : γ}
{f : α → γ}
(hf : filter.tendsto f (filter.comap i (nhds b)) (nhds c)) :
theorem
dense_inducing.extend_eq_at
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
{i : α → β}
(di : dense_inducing i)
[topological_space γ]
[t2_space γ]
{f : α → γ}
{a : α}
(hf : continuous_at f a) :
theorem
dense_inducing.extend_eq_at'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
{i : α → β}
(di : dense_inducing i)
[topological_space γ]
[t2_space γ]
{f : α → γ}
{a : α}
(c : γ)
(hf : filter.tendsto f (nhds a) (nhds c)) :
theorem
dense_inducing.extend_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
{i : α → β}
(di : dense_inducing i)
[topological_space γ]
[t2_space γ]
{f : α → γ}
(hf : continuous f)
(a : α) :
theorem
dense_inducing.extend_eq'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
{i : α → β}
[topological_space γ]
[t2_space γ]
{f : α → γ}
(di : dense_inducing 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
dense_inducing.extend_unique_at
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
{i : α → β}
[topological_space γ]
[t2_space γ]
{b : β}
{f : α → γ}
{g : β → γ}
(di : dense_inducing i)
(hf : ∀ᶠ (x : α) in filter.comap i (nhds b), g (i x) = f x)
(hg : continuous_at g b) :
theorem
dense_inducing.extend_unique
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
{i : α → β}
[topological_space γ]
[t2_space γ]
{f : α → γ}
{g : β → γ}
(di : dense_inducing i)
(hf : ∀ (x : α), g (i x) = f x)
(hg : continuous g) :
theorem
dense_inducing.continuous_at_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
{i : α → β}
[topological_space γ]
[t3_space γ]
{b : β}
{f : α → γ}
(di : dense_inducing i)
(hf : ∀ᶠ (x : β) in nhds b, ∃ (c : γ), filter.tendsto f (filter.comap i (nhds x)) (nhds c)) :
continuous_at (di.extend f) b
theorem
dense_inducing.continuous_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
{i : α → β}
[topological_space γ]
[t3_space γ]
{f : α → γ}
(di : dense_inducing i)
(hf : ∀ (b : β), ∃ (c : γ), filter.tendsto f (filter.comap i (nhds b)) (nhds c)) :
continuous (di.extend f)
structure
dense_embedding
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α → β) :
Prop
- to_dense_inducing : dense_inducing e
- inj : function.injective e
A dense embedding is an embedding with dense image.
theorem
dense_embedding.mk'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α → β)
(c : continuous e)
(dense : dense_range e)
(inj : function.injective e)
(H : ∀ (a : α) (s : set α), s ∈ nhds a → (∃ (t : set β) (H : t ∈ nhds (e a)), ∀ (b : α), e b ∈ t → b ∈ s)) :
theorem
dense_embedding.inj_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : α → β}
(de : dense_embedding e)
{x y : α} :
theorem
dense_embedding.to_embedding
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : α → β}
(de : dense_embedding e) :
@[protected]
theorem
dense_embedding.separable_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : α → β}
(de : dense_embedding e)
[topological_space.separable_space α] :
If the domain of a dense_embedding is a separable space, then so is its codomain.
@[protected]
theorem
dense_embedding.prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{e₁ : α → β}
{e₂ : γ → δ}
(de₁ : dense_embedding e₁)
(de₂ : dense_embedding e₂) :
dense_embedding (λ (p : α × γ), (e₁ p.fst, e₂ p.snd))
The product of two dense embeddings is a dense embedding.
@[simp]
theorem
dense_embedding.subtype_emb_coe
{β : Type u_2}
[topological_space β]
{α : Type u_1}
(p : α → Prop)
(e : α → β)
(x : {x // p x}) :
↑(dense_embedding.subtype_emb p e x) = e ↑x
def
dense_embedding.subtype_emb
{β : Type u_2}
[topological_space β]
{α : Type u_1}
(p : α → Prop)
(e : α → β)
(x : {x // p x}) :
The dense embedding of a subtype inside its closure.
Equations
- dense_embedding.subtype_emb p e x = ⟨e ↑x, _⟩
@[protected]
theorem
dense_embedding.subtype
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : α → β}
(de : dense_embedding e)
(p : α → Prop) :
theorem
dense_embedding.dense_image
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : α → β}
(de : dense_embedding e)
{s : set α} :
theorem
is_closed_property
{α : Type u_1}
{β : Type u_2}
[topological_space β]
{e : α → β}
{p : β → Prop}
(he : dense_range e)
(hp : is_closed {x : β | p x})
(h : ∀ (a : α), p (e a))
(b : β) :
p b
theorem
is_closed_property2
{α : Type u_1}
{β : Type u_2}
[topological_space β]
{e : α → β}
{p : β → β → Prop}
(he : dense_range e)
(hp : is_closed {q : β × β | p q.fst q.snd})
(h : ∀ (a₁ a₂ : α), p (e a₁) (e a₂))
(b₁ b₂ : β) :
p b₁ b₂
theorem
dense_range.induction_on
{α : Type u_1}
{β : Type u_2}
[topological_space β]
{e : α → β}
(he : dense_range e)
{p : β → Prop}
(b₀ : β)
(hp : is_closed {b : β | p b})
(ih : ∀ (a : α), p (e a)) :
p b₀
theorem
dense_range.induction_on₂
{α : Type u_1}
{β : Type u_2}
[topological_space β]
{e : α → β}
{p : β → β → Prop}
(he : dense_range e)
(hp : is_closed {q : β × β | p q.fst q.snd})
(h : ∀ (a₁ a₂ : α), p (e a₁) (e a₂))
(b₁ b₂ : β) :
p b₁ b₂
theorem
dense_range.equalizer
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space β]
[topological_space γ]
[t2_space γ]
{f : α → β}
(hfd : dense_range 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.has_basis.has_basis_of_dense_inducing
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[t3_space β]
{ι : Type u_3}
{s : ι → set α}
{p : ι → Prop}
{x : α}
(h : (nhds x).has_basis p s)
{f : α → β}
(hf : dense_inducing f) :