mathlib3 documentation

topology.dense_embedding

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:

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

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.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) :
closure (i '' s) nhds (i a)
theorem dense_inducing.dense_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {i : α β} (di : dense_inducing i) {s : set α} :
dense (i '' s) dense s
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]

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) :
 γ -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 : β) :
theorem dense_inducing.comap_nhds_ne_bot {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {i : α β} (di : dense_inducing i) (b : β) :
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
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)) :
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 : α} (hf : continuous_at f a) :
di.extend f (i a) = 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)) :
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 : α) :
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 : α β} [topological_space γ] [t2_space γ] {f : α γ} (di : dense_inducing i) (hf : (b : β), (c : γ), filter.tendsto f (filter.comap i (nhds b)) (nhds c)) (a : α) :
di.extend 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 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) :
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) (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} [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)) :
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)) :
theorem dense_inducing.mk' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (i : α β) (c : continuous i) (dense : (x : β), x closure (set.range i)) (H : (a : α) (s : set α), s nhds a ( (t : set β) (H : t nhds (i a)), (b : α), i b t b s)) :
structure dense_embedding {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : α β) :
Prop

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 : α} :
e x = e y x = y
theorem dense_embedding.to_embedding {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : α β} (de : dense_embedding e) :
@[protected]

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}) :
def dense_embedding.subtype_emb {β : Type u_2} [topological_space β] {α : 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
@[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 α} :
dense (e '' s) dense s
theorem dense.dense_embedding_coe {α : Type u_1} [topological_space α] {s : set α} (hs : dense s) :
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₀ : β) (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.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 : β γ} (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) :
(nhds (f x)).has_basis p (λ (i : ι), closure (f '' s i))