# mathlibdocumentation

topology.dense_embedding

# Dense embeddings #

This file defines three properties of functions:

• dense_range f means f has dense image;
• dense_inducing i means i is also inducing;
• dense_embedding e means e is also an embedding.

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).

structure dense_inducing {α : Type u_1} {β : Type u_2} (i : α → β) :
Prop
• to_inducing :
• dense :

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} {i : α → β} (di : dense_inducing i) (a : α) :
𝓝 a = (𝓝 (i a))
theorem dense_inducing.continuous {α : Type u_1} {β : Type u_2} {i : α → β} (di : dense_inducing i) :
theorem dense_inducing.closure_range {α : Type u_1} {β : Type u_2} {i : α → β} (di : dense_inducing i) :
theorem dense_inducing.preconnected_space {α : Type u_1} {β : Type u_2} {i : α → β} (di : dense_inducing i) :
theorem dense_inducing.closure_image_mem_nhds {α : Type u_1} {β : Type u_2} {i : α → β} {s : set α} {a : α} (di : dense_inducing i) (hs : s 𝓝 a) :
closure (i '' s) 𝓝 (i a)
theorem dense_inducing.dense_image {α : Type u_1} {β : Type u_2} {i : α → β} (di : dense_inducing i) {s : set α} :
dense (i '' s)
theorem dense_inducing.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {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

theorem dense_inducing.separable_space {α : Type u_1} {β : Type u_2} {i : α → β} (di : dense_inducing i)  :

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} {i : α → β} {f : γ → α} {g : γ → δ} {h : δ → β} {d : δ} {a : α} (di : dense_inducing i) (H : (𝓝 d) (𝓝 (i a))) (comm : h g = i f) :
(𝓝 d)) (𝓝 a)

γ -f→ α g↓ ↓e δ -h→ β

theorem dense_inducing.nhds_within_ne_bot {α : Type u_1} {β : Type u_2} {i : α → β} (di : dense_inducing i) (b : β) :
theorem dense_inducing.comap_nhds_ne_bot {α : Type u_1} {β : Type u_2} {i : α → β} (di : dense_inducing i) (b : β) :
(𝓝 b)).ne_bot
def dense_inducing.extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {i : α → β} (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
theorem dense_inducing.extend_eq_of_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {i : α → β} (di : dense_inducing i) [t2_space γ] {b : β} {c : γ} {f : α → γ} (hf : (𝓝 b)) (𝓝 c)) :
di.extend f b = c
theorem dense_inducing.extend_eq_at {α : Type u_1} {β : Type u_2} {γ : Type u_3} {i : α → β} (di : dense_inducing i) [t2_space γ] {f : α → γ} (a : α) (hf : a) :
di.extend f (i a) = f a
theorem dense_inducing.extend_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {i : α → β} (di : dense_inducing i) [t2_space γ] {f : α → γ} (hf : continuous f) (a : α) :
di.extend f (i a) = f a
theorem dense_inducing.extend_unique_at {α : Type u_1} {β : Type u_2} {γ : Type u_3} {i : α → β} [t2_space γ] {b : β} {f : α → γ} {g : β → γ} (di : dense_inducing i) (hf : ∀ᶠ (x : α) in (𝓝 b), g (i x) = f x) (hg : b) :
di.extend f b = g b
theorem dense_inducing.extend_unique {α : Type u_1} {β : Type u_2} {γ : Type u_3} {i : α → β} [t2_space γ] {f : α → γ} {g : β → γ} (di : dense_inducing i) (hf : ∀ (x : α), g (i x) = f x) (hg : continuous g) :
di.extend f = g
theorem dense_inducing.continuous_at_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {i : α → β} {b : β} {f : α → γ} (di : dense_inducing i) (hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), (𝓝 x)) (𝓝 c)) :
theorem dense_inducing.continuous_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {i : α → β} {f : α → γ} (di : dense_inducing i) (hf : ∀ (b : β), ∃ (c : γ), (𝓝 b)) (𝓝 c)) :
theorem dense_inducing.mk' {α : Type u_1} {β : Type u_2} (i : α → β) (c : continuous i) (dense : ∀ (x : β), x closure (set.range i)) (H : ∀ (a : α) (s : set α), s 𝓝 a(∃ (t : set β) (H : t 𝓝 (i a)), ∀ (b : α), i b tb s)) :
structure dense_embedding {α : Type u_1} {β : Type u_2} (e : α → β) :
Prop
• to_dense_inducing :
• inj :

A dense embedding is an embedding with dense image.

theorem dense_embedding.mk' {α : Type u_1} {β : Type u_2} (e : α → β) (c : continuous e) (dense : dense_range e) (inj : function.injective e) (H : ∀ (a : α) (s : set α), s 𝓝 a(∃ (t : set β) (H : t 𝓝 (e a)), ∀ (b : α), e b tb s)) :
theorem dense_embedding.inj_iff {α : Type u_1} {β : Type u_2} {e : α → β} (de : dense_embedding e) {x y : α} :
e x = e y x = y
theorem dense_embedding.to_embedding {α : Type u_1} {β : Type u_2} {e : α → β} (de : dense_embedding e) :
theorem dense_embedding.separable_space {α : Type u_1} {β : Type u_2} {e : α → β} (de : dense_embedding e)  :

If the domain of a dense_embedding is a separable space, then so is its codomain.

theorem dense_embedding.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {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} {α : Type u_1} (p : α → Prop) (e : α → β) (x : {x // p x}) :
x) = e x
def dense_embedding.subtype_emb {β : Type u_2} {α : Type u_1} (p : α → Prop) (e : α → β) (x : {x // p x}) :
{x // x closure (e '' {x : α | p x})}

The dense embedding of a subtype inside its closure.

Equations
theorem dense_embedding.subtype {α : Type u_1} {β : Type u_2} {e : α → β} (de : dense_embedding e) (p : α → Prop) :
theorem dense_embedding.dense_image {α : Type u_1} {β : Type u_2} {e : α → β} (de : dense_embedding e) {s : set α} :
dense (e '' s)
theorem dense.dense_embedding_coe {α : Type u_1} {s : set α} (hs : dense s) :
theorem is_closed_property {α : Type u_1} {β : Type u_2} {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} {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} {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} {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} {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} {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} [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.