# 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}  :
(α → β) → 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 : α → β} :

theorem dense_inducing.closure_range {α : Type u_1} {β : Type u_2} {i : α → β} :

theorem dense_inducing.self_sub_closure_image_preimage_of_open {α : Type u_1} {β : Type u_2} {i : α → β} {s : set β} :
s closure (i '' (i ⁻¹' s))

theorem dense_inducing.closure_image_nhds_of_nhds {α : Type u_1} {β : Type u_2} {i : α → β} {s : set α} {a : α} :
s 𝓝 aclosure (i '' s) 𝓝 (i a)

theorem dense_inducing.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {e₁ : α → β} {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 : α} :
(𝓝 d) (𝓝 (i a))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 : α → β}  :
(α → γ)β → γ

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 : α → γ} :
(𝓝 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 : α) :
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) :
(∀ᶠ (x : α) in (𝓝 b), g (i x) = f x)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) :
(∀ (x : α), g (i x) = f x)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) :
(∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), (𝓝 x)) (𝓝 c))continuous_at (di.extend f) b

theorem dense_inducing.continuous_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {i : α → β} {f : α → γ} (di : dense_inducing i) :
(∀ (b : β), ∃ (c : γ), (𝓝 b)) (𝓝 c))continuous (di.extend f)

theorem dense_inducing.mk' {α : Type u_1} {β : Type u_2} (i : α → β) :
(∀ (x : β), x closure (set.range i))(∀ (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}  :
(α → β) → 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 : α → β) :
(∀ (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 : α → β} :

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₂ : γ → δ} :
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} {α : Type u_1} (p : α → Prop) (e : α → β) :
{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 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₀ : β) :
is_closed {b : β | p b}(∀ (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 : β → γ} :
g f = h fg = h

Two continuous functions to a t2-space that agree on the dense range of a function are equal.