# Documentation

Mathlib.Topology.DenseEmbedding

# Dense embeddings #

This file defines three properties of functions:

• DenseRange f means f has dense image;
• DenseInducing i means i is also Inducing, namely it induces the topology on its codomain;
• DenseEmbedding e means e is further an Embedding, namely it is injective and Inducing.

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} [] [] (i : αβ) extends :

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} [] [] {i : αβ} (di : ) (a : α) :
nhds a = Filter.comap i (nhds (i a))
theorem DenseInducing.continuous {α : Type u_1} {β : Type u_2} [] [] {i : αβ} (di : ) :
theorem DenseInducing.closure_range {α : Type u_1} {β : Type u_2} [] [] {i : αβ} (di : ) :
closure () = Set.univ
theorem DenseInducing.preconnectedSpace {α : Type u_1} {β : Type u_2} [] [] {i : αβ} (di : ) :
theorem DenseInducing.closure_image_mem_nhds {α : Type u_1} {β : Type u_2} [] [] {i : αβ} {s : Set α} {a : α} (di : ) (hs : s nhds a) :
closure (i '' s) nhds (i a)
theorem DenseInducing.dense_image {α : Type u_1} {β : Type u_2} [] [] {i : αβ} (di : ) {s : Set α} :
Dense (i '' s)
theorem DenseInducing.interior_compact_eq_empty {α : Type u_1} {β : Type u_2} [] [] {i : αβ} [] (di : ) (hd : Dense ()) {s : Set α} (hs : ) :

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} [] [] [] [] {e₁ : αβ} {e₂ : γδ} (de₁ : ) (de₂ : ) :
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} [] [] {i : αβ} (di : ) :

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} [] [] {i : αβ} [] {f : γα} {g : γδ} {h : δβ} {d : δ} {a : α} (di : ) (H : Filter.Tendsto h (nhds d) (nhds (i a))) (comm : h g = i f) :
 γ -f→ α
g↓     ↓e
δ -h→ β

theorem DenseInducing.nhdsWithin_neBot {α : Type u_1} {β : Type u_2} [] [] {i : αβ} (di : ) (b : β) :
theorem DenseInducing.comap_nhds_neBot {α : Type u_1} {β : Type u_2} [] [] {i : αβ} (di : ) (b : β) :
def DenseInducing.extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {i : αβ} [] (di : ) (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.

Instances For
theorem DenseInducing.extend_eq_of_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {i : αβ} (di : ) [] [] {b : β} {c : γ} {f : αγ} (hf : Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c)) :
= c
theorem DenseInducing.extend_eq_at {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {i : αβ} (di : ) [] [] {f : αγ} {a : α} (hf : ) :
DenseInducing.extend di f (i a) = f a
theorem DenseInducing.extend_eq_at' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {i : αβ} (di : ) [] [] {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} [] [] {i : αβ} (di : ) [] [] {f : αγ} (hf : ) (a : α) :
DenseInducing.extend di f (i a) = f a
theorem DenseInducing.extend_eq' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {i : αβ} [] [] {f : αγ} (di : ) (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} [] [] {i : αβ} [] [] {b : β} {f : αγ} {g : βγ} (di : ) (hf : ∀ᶠ (x : α) in Filter.comap i (nhds b), g (i x) = f x) (hg : ) :
= g b
theorem DenseInducing.extend_unique {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {i : αβ} [] [] {f : αγ} {g : βγ} (di : ) (hf : ∀ (x : α), g (i x) = f x) (hg : ) :
= g
theorem DenseInducing.continuousAt_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {i : αβ} [] [] {b : β} {f : αγ} (di : ) (hf : ∀ᶠ (x : β) in nhds b, c, Filter.Tendsto f (Filter.comap i (nhds x)) (nhds c)) :
theorem DenseInducing.continuous_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {i : αβ} [] [] {f : αγ} (di : ) (hf : ∀ (b : β), c, Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c)) :
theorem DenseInducing.mk' {α : Type u_1} {β : Type u_2} [] [] (i : αβ) (c : ) (dense : ∀ (x : β), x closure ()) (H : ∀ (a : α) (s : Set α), s nhds at, t nhds (i a) ∀ (b : α), i b tb s) :
structure DenseEmbedding {α : Type u_1} {β : Type u_2} [] [] (e : αβ) extends :

A dense embedding is an embedding with dense image.

Instances For
theorem DenseEmbedding.mk' {α : Type u_1} {β : Type u_2} [] [] (e : αβ) (c : ) (dense : ) (inj : ) (H : ∀ (a : α) (s : Set α), s nhds at, t nhds (e a) ∀ (b : α), e b tb s) :
theorem DenseEmbedding.inj_iff {α : Type u_1} {β : Type u_2} [] [] {e : αβ} (de : ) {x : α} {y : α} :
e x = e y x = y
theorem DenseEmbedding.to_embedding {α : Type u_1} {β : Type u_2} [] [] {e : αβ} (de : ) :
theorem DenseEmbedding.separableSpace {α : Type u_1} {β : Type u_2} [] [] {e : αβ} (de : ) :

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} [] [] [] [] {e₁ : αβ} {e₂ : γδ} (de₁ : ) (de₂ : ) :
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} [] {α : Type u_5} (p : αProp) (e : αβ) (x : { x // p x }) :
↑() = e x
def DenseEmbedding.subtypeEmb {β : Type u_2} [] {α : Type u_5} (p : αProp) (e : αβ) (x : { x // p x }) :
{ x // x closure (e '' {x | p x}) }

The dense embedding of a subtype inside its closure.

Instances For
theorem DenseEmbedding.subtype {α : Type u_1} {β : Type u_2} [] [] {e : αβ} (de : ) (p : αProp) :
theorem DenseEmbedding.dense_image {α : Type u_1} {β : Type u_2} [] [] {e : αβ} (de : ) {s : Set α} :
Dense (e '' s)
theorem denseEmbedding_id {α : Type u_5} [] :
theorem Dense.denseEmbedding_val {α : Type u_1} [] {s : Set α} (hs : ) :
DenseEmbedding Subtype.val
theorem isClosed_property {α : Type u_1} {β : Type u_2} [] {e : αβ} {p : βProp} (he : ) (hp : IsClosed {x | p x}) (h : (a : α) → p (e a)) (b : β) :
p b
theorem isClosed_property2 {α : Type u_1} {β : Type u_2} [] {e : αβ} {p : ββProp} (he : ) (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} [] {e : αβ} {p : βββProp} (he : ) (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} [] {e : αβ} (he : ) {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} [] {e : αβ} {p : ββProp} (he : ) (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} [] {e : αβ} {p : βββProp} (he : ) (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} [] [] [] {f : αβ} (hfd : ) {g : βγ} {h : βγ} (hg : ) (hh : ) (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} [] [] [] {ι : Type u_5} {s : ιSet α} {p : ιProp} {x : α} (h : Filter.HasBasis (nhds x) p s) {f : αβ} (hf : ) :
Filter.HasBasis (nhds (f x)) p fun i => closure (f '' s i)