Dense embeddings
This file defines three properties of functions:
dense_range fmeansfhas dense image;dense_inducing imeansiis alsoinducing;dense_embedding emeanseis also anembedding.
The main theorem continuous_extend gives a criterion for a function
f : X → Z to a regular (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).
f : α → β has dense range if its range (image) is a dense subset of β.
Equations
- dense_range f = ∀ (x : β), x ∈ closure (set.range f)
theorem
dense_range_iff_closure_range
{α : Type u_1}
{β : Type u_2}
[topological_space β]
{f : α → β} :
theorem
dense_range.closure_range
{α : Type u_1}
{β : Type u_2}
[topological_space β]
{f : α → β} :
dense_range f → closure (set.range f) = set.univ
theorem
dense_range.nhds_within_ne_bot
{α : Type u_1}
{β : Type u_2}
[topological_space β]
{f : α → β}
(h : dense_range f)
(x : β) :
(nhds_within x (set.range f)).ne_bot
theorem
dense_range.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space β]
[topological_space γ]
{f : α → β}
(g : β → γ) :
dense_range g → dense_range f → continuous g → dense_range (g ∘ f)
def
dense_range.inhabited
{α : Type u_1}
{β : Type u_2}
[topological_space β]
{f : α → β} :
dense_range f → β → inhabited α
If f : α → β has dense range and β contains some element, then α must too.
Equations
- df.inhabited b = {default := classical.choice _}
theorem
dense_range.nonempty
{α : Type u_1}
{β : Type u_2}
[topological_space β]
{f : α → β} :
dense_range f → (nonempty α ↔ nonempty β)
theorem
dense_range.prod
{β : Type u_2}
{γ : Type u_3}
[topological_space β]
[topological_space γ]
{ι : Type u_1}
{κ : Type u_4}
{f : ι → β}
{g : κ → γ} :
dense_range f → dense_range g → dense_range (λ (p : ι × κ), (f p.fst, g p.snd))
structure
dense_inducing
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
(α → β) → 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))
theorem
dense_inducing.continuous
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β} :
dense_inducing i → continuous i
theorem
dense_inducing.closure_range
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β} :
dense_inducing i → closure (set.range i) = set.univ
theorem
dense_inducing.self_sub_closure_image_preimage_of_open
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β}
{s : set β} :
theorem
dense_inducing.closure_image_nhds_of_nhds
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{i : α → β}
{s : set α}
{a : α} :
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₂ : γ → δ} :
dense_inducing e₁ → dense_inducing e₂ → dense_inducing (λ (p : α × γ), (e₁ p.fst, e₂ p.snd))
The product of two dense inducings is a dense inducing
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 : α} :
dense_inducing i → filter.tendsto h (nhds d) (nhds (i a)) → h ∘ g = i ∘ f → filter.tendsto f (filter.comap g (nhds d)) (nhds a)
γ -f→ α g↓ ↓e δ -h→ β
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
def
dense_inducing.extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
{i : α → β}
[topological_space γ] :
dense_inducing i → (α → γ) → β → γ
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 : α → γ} :
filter.tendsto f (filter.comap i (nhds b)) (nhds c) → di.extend f b = 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 : α) :
continuous_at f a → di.extend f (i a) = f a
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_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) :
(∀ᶠ (x : α) in filter.comap i (nhds b), g (i x) = f x) → continuous_at g b → di.extend f b = 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) :
(∀ (x : α), g (i x) = f x) → continuous g → di.extend f = g
theorem
dense_inducing.continuous_at_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
{i : α → β}
[topological_space γ]
[regular_space γ]
{b : β}
{f : α → γ}
(di : dense_inducing i) :
(∀ᶠ (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 γ]
[regular_space γ]
{f : α → γ}
(di : dense_inducing i) :
(∀ (b : β), ∃ (c : γ), filter.tendsto f (filter.comap i (nhds b)) (nhds c)) → continuous (di.extend f)
theorem
dense_inducing.mk'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(i : α → β) :
structure
dense_embedding
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
(α → β) → 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 : α → β) :
continuous e → (∀ (x : β), x ∈ closure (set.range e)) → function.injective e → (∀ (a : α) (s : set α), s ∈ nhds a → (∃ (t : set β) (H : t ∈ nhds (e a)), ∀ (b : α), e b ∈ t → b ∈ s)) → dense_embedding e
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 : α → β} :
dense_embedding e → embedding e
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₂ : γ → δ} :
dense_embedding e₁ → dense_embedding e₂ → dense_embedding (λ (p : α × γ), (e₁ p.fst, e₂ p.snd))
The product of two dense embeddings is a dense embedding
def
dense_embedding.subtype_emb
{β : Type u_2}
[topological_space β]
{α : Type u_1}
(p : α → Prop)
(e : α → β) :
The dense embedding of a subtype inside its closure.
Equations
- dense_embedding.subtype_emb p e x = ⟨e ↑x, _⟩
theorem
dense_embedding.subtype
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : α → β}
(de : dense_embedding e)
(p : α → Prop) :
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
is_closed_property3
{α : Type u_1}
{β : Type u_2}
[topological_space β]
{e : α → β}
{p : β → β → β → Prop}
(he : dense_range e)
(hp : is_closed {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
dense_range.induction_on
{α : Type u_1}
{β : Type u_2}
[topological_space β]
{e : α → β}
(he : dense_range e)
{p : β → Prop}
(b₀ : β) :
is_closed {b : β | p b} → (∀ (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.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.fst q.snd.snd})
(h : ∀ (a₁ a₂ a₃ : α), p (e a₁) (e a₂) (e a₃))
(b₁ b₂ b₃ : β) :
p b₁ 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 : β → γ} :
continuous g → continuous 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.