# Dense embeddings #

This file defines three properties of functions:

- `DenseRange f` means `f` has dense image;
- `IsDenseInducing i` means `i` is also inducing, namely it induces the topology on its codomain;
- `IsDenseEmbedding 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 `IsDenseInducing` (not necessarily injective).

source
structure IsDenseInducing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (i : α → β) extends Topology.IsInducing 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 `β`.

- eq_induced : inst✝ = TopologicalSpace.induced i inst✝¹
- dense : DenseRange i

  The range of a dense inducing map is a dense set.

Instances For

source
theorem Dense.isDenseInducing_val {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : Dense s) :
IsDenseInducing Subtype.val
source
theorem IsDenseInducing.isInducing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) :
Topology.IsInducing i
source
theorem IsDenseInducing.nhds_eq_comap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) (a : α) :
nhds a = Filter.comap i (nhds (i a))
source
theorem IsDenseInducing.continuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) :
Continuous i
source
theorem IsDenseInducing.closure_range {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) :
closure (Set.range i) = Set.univ
source
theorem IsDenseInducing.preconnectedSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [PreconnectedSpace α] (di : IsDenseInducing i) :
PreconnectedSpace β
source
theorem IsDenseInducing.closure_image_mem_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} {s : Set α} {a : α} (di : IsDenseInducing i) (hs : s ∈ nhds a) :
closure (i '' s) ∈ nhds (i a)
source
theorem IsDenseInducing.dense_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) {s : Set α} :
Dense (i '' s) ↔ Dense s
source
theorem IsDenseInducing.interior_compact_eq_empty {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [T2Space β] (di : IsDenseInducing i) (hd : Dense (Set.range i)ᶜ) {s : Set α} (hs : IsCompact s) :
interior s = ∅

If `i : α → β` is a dense embedding with dense complement of the range, then any compact set in `α` has empty interior.

source
theorem IsDenseInducing.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {e₁ : α → β} {e₂ : γ → δ} (de₁ : IsDenseInducing e₁) (de₂ : IsDenseInducing e₂) :
IsDenseInducing (Prod.map e₁ e₂)

The product of two dense inducings is a dense inducing

source
theorem IsDenseInducing.separableSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace.SeparableSpace α] (di : IsDenseInducing i) :
TopologicalSpace.SeparableSpace β

If the domain of a `IsDenseInducing` map is a separable space, then so is the codomain.

source
theorem IsDenseInducing.tendsto_comap_nhds_nhds {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace δ] {f : γ → α} {g : γ → δ} {h : δ → β} {d : δ} {a : α} (di : IsDenseInducing i) (H : Filter.Tendsto h (nhds d) (nhds (i a))) (comm : h ∘ g = i ∘ f) :
Filter.Tendsto f (Filter.comap g (nhds d)) (nhds a)

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

source
theorem IsDenseInducing.nhdsWithin_neBot {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) (b : β) :
(nhdsWithin b (Set.range i)).NeBot
source
theorem IsDenseInducing.comap_nhds_neBot {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) (b : β) :
(Filter.comap i (nhds b)).NeBot
source
theorem Dense.comap_val_nhds_neBot {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : Dense s) (a : α) :
(Filter.comap Subtype.val (nhds a)).NeBot
source
def IsDenseInducing.extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] (di : IsDenseInducing i) (f : α → γ) (b : β) :
γ

If `i : α → β` is a dense inducing, then any function `f : α → γ` "extends" to a function `g = IsDenseInducing.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 = limUnder (Filter.comap i (nhds b)) f

Instances For

source
theorem IsDenseInducing.tendsto_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (hf : ContinuousAt f a) :
Filter.Tendsto f (nhds a) (nhds (di.extend f (i a)))
source
theorem IsDenseInducing.inseparable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [R1Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (hf : ContinuousAt f a) :
Inseparable (di.extend f (i a)) (f a)
source
theorem IsDenseInducing.extend_eq_of_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T2Space γ] (di : IsDenseInducing i) {b : β} {c : γ} {f : α → γ} (hf : Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c)) :
di.extend f b = c
source
theorem IsDenseInducing.extend_eq_at {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T2Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (hf : ContinuousAt f a) :
di.extend f (i a) = f a
source
theorem IsDenseInducing.extend_eq_at' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T2Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (c : γ) (hf : Filter.Tendsto f (nhds a) (nhds c)) :
di.extend f (i a) = f a
source
theorem IsDenseInducing.extend_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T2Space γ] (di : IsDenseInducing i) {f : α → γ} (hf : Continuous f) (a : α) :
di.extend f (i a) = f a
source
theorem IsDenseInducing.extend_eq' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T2Space γ] {f : α → γ} (di : IsDenseInducing 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.

source
theorem IsDenseInducing.extend_unique_at {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T2Space γ] {b : β} {f : α → γ} {g : β → γ} (di : IsDenseInducing i) (hf : ∀ᶠ (x : α) in Filter.comap i (nhds b), g (i x) = f x) (hg : ContinuousAt g b) :
di.extend f b = g b
source
theorem IsDenseInducing.extend_unique {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T2Space γ] {f : α → γ} {g : β → γ} (di : IsDenseInducing i) (hf : ∀ (x : α), g (i x) = f x) (hg : Continuous g) :
di.extend f = g
source
theorem IsDenseInducing.continuousAt_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T3Space γ] {b : β} {f : α → γ} (di : IsDenseInducing i) (hf : ∀ᶠ (x : β) in nhds b, ∃ (c : γ), Filter.Tendsto f (Filter.comap i (nhds x)) (nhds c)) :
ContinuousAt (di.extend f) b
source
theorem IsDenseInducing.continuous_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T3Space γ] {f : α → γ} (di : IsDenseInducing i) (hf : ∀ (b : β), ∃ (c : γ), Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c)) :
Continuous (di.extend f)
source
theorem IsDenseInducing.mk' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (i : α → β) (c : Continuous i) (dense : ∀ (x : β), x ∈ closure (Set.range i)) (H : ∀ (a : α), ∀ s ∈ nhds a, ∃ t ∈ nhds (i a), ∀ (b : α), i b ∈ t → b ∈ s) :
IsDenseInducing i
source
noncomputable def Dense.extend {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (hs : Dense s) (f : ↑s → β) :
α → β

This is a shortcut for `hs.isDenseInducing_val.extend f`. It is useful because if `s : Set α` is dense then the coercion `(↑) : s → α` automatically satisfies `IsUniformInducing` and `IsDenseInducing` so this gives access to the theorems satisfied by a uniform extension by simply mentioning the density hypothesis.

Equations

- hs.extend f = ⋯.extend f

Instances For

source
theorem Dense.extend_eq_of_tendsto {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T2Space β] (hs : Dense s) {a : α} {b : β} (hf : Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b)) :
hs.extend f a = b
source
theorem Dense.extend_eq_at {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} [T2Space β] (hs : Dense s) {f : ↑s → β} {x : ↑s} (hf : ContinuousAt f x) :
hs.extend f ↑x = f x
source
theorem Dense.extend_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T2Space β] (hs : Dense s) (hf : Continuous f) (x : ↑s) :
hs.extend f ↑x = f x
source
theorem Dense.extend_unique_at {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T2Space β] {a : α} {g : α → β} (hs : Dense s) (hf : ∀ᶠ (x : ↑s) in Filter.comap Subtype.val (nhds a), g ↑x = f x) (hg : ContinuousAt g a) :
hs.extend f a = g a
source
theorem Dense.extend_unique {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T2Space β] {g : α → β} (hs : Dense s) (hf : ∀ (x : ↑s), g ↑x = f x) (hg : Continuous g) :
hs.extend f = g
source
theorem Dense.continuousAt_extend {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T3Space β] {a : α} (hs : Dense s) (hf : ∀ᶠ (x : α) in nhds a, ∃ (b : β), Filter.Tendsto f (Filter.comap Subtype.val (nhds x)) (nhds b)) :
ContinuousAt (hs.extend f) a
source
theorem Dense.continuous_extend {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T3Space β] (hs : Dense s) (hf : ∀ (a : α), ∃ (b : β), Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b)) :
Continuous (hs.extend f)
source
structure IsDenseEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α → β) extends IsDenseInducing e :
Prop

A dense embedding is an embedding with dense image.

- eq_induced : inst✝ = TopologicalSpace.induced e inst✝¹
- dense : DenseRange e
- injective : Function.Injective e

  A dense embedding is injective.

Instances For

source
theorem IsDenseEmbedding.mk' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α → β) (c : Continuous e) (dense : DenseRange e) (injective : Function.Injective e) (H : ∀ (a : α), ∀ s ∈ nhds a, ∃ t ∈ nhds (e a), ∀ (b : α), e b ∈ t → b ∈ s) :
IsDenseEmbedding e
source
theorem IsDenseEmbedding.isDenseInducing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : α → β} (de : IsDenseEmbedding e) :
IsDenseInducing e
source
theorem IsDenseEmbedding.inj_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : α → β} (de : IsDenseEmbedding e) {x y : α} :
e x = e y ↔ x = y
source
theorem IsDenseEmbedding.isEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : α → β} (de : IsDenseEmbedding e) :
Topology.IsEmbedding e
source
theorem IsDenseEmbedding.separableSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : α → β} [TopologicalSpace.SeparableSpace α] (de : IsDenseEmbedding e) :
TopologicalSpace.SeparableSpace β

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

source
theorem IsDenseEmbedding.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {e₁ : α → β} {e₂ : γ → δ} (de₁ : IsDenseEmbedding e₁) (de₂ : IsDenseEmbedding e₂) :
IsDenseEmbedding fun (p : α × γ) => (e₁ p.1, e₂ p.2)

The product of two dense embeddings is a dense embedding.

source
def IsDenseEmbedding.subtypeEmb {β : Type u_2} [TopologicalSpace β] {α : 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.

Equations

- IsDenseEmbedding.subtypeEmb p e x = ⟨e ↑x, ⋯⟩

Instances For

source
@[simp]
theorem IsDenseEmbedding.subtypeEmb_coe {β : Type u_2} [TopologicalSpace β] {α : Type u_5} (p : α → Prop) (e : α → β) (x : { x : α // p x }) :
↑(subtypeEmb p e x) = e ↑x
source
theorem IsDenseEmbedding.subtype {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : α → β} (de : IsDenseEmbedding e) (p : α → Prop) :
IsDenseEmbedding (subtypeEmb p e)
source
theorem IsDenseEmbedding.dense_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : α → β} (de : IsDenseEmbedding e) {s : Set α} :
Dense (e '' s) ↔ Dense s
source
theorem IsDenseEmbedding.id {α : Type u_5} [TopologicalSpace α] :
IsDenseEmbedding id
source
theorem Dense.isDenseEmbedding_val {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : Dense s) :
IsDenseEmbedding Subtype.val
source
theorem isClosed_property {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {e : α → β} {p : β → Prop} (he : DenseRange e) (hp : IsClosed {x : β | p x}) (h : ∀ (a : α), p (e a)) (b : β) :
p b
source
theorem isClosed_property2 {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {e : α → β} {p : β → β → Prop} (he : DenseRange e) (hp : IsClosed {q : β × β | p q.1 q.2}) (h : ∀ (a₁ a₂ : α), p (e a₁) (e a₂)) (b₁ b₂ : β) :
p b₁ b₂
source
theorem isClosed_property3 {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {e : α → β} {p : β → β → β → Prop} (he : DenseRange e) (hp : IsClosed {q : β × β × β | p q.1 q.2.1 q.2.2}) (h : ∀ (a₁ a₂ a₃ : α), p (e a₁) (e a₂) (e a₃)) (b₁ b₂ b₃ : β) :
p b₁ b₂ b₃
source
theorem DenseRange.induction_on {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {e : α → β} (he : DenseRange e) {p : β → Prop} (b₀ : β) (hp : IsClosed {b : β | p b}) (ih : ∀ (a : α), p (e a)) :
p b₀
source
theorem DenseRange.induction_on₂ {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {e : α → β} {p : β → β → Prop} (he : DenseRange e) (hp : IsClosed {q : β × β | p q.1 q.2}) (h : ∀ (a₁ a₂ : α), p (e a₁) (e a₂)) (b₁ b₂ : β) :
p b₁ b₂
source
theorem DenseRange.induction_on₃ {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {e : α → β} {p : β → β → β → Prop} (he : DenseRange e) (hp : IsClosed {q : β × β × β | p q.1 q.2.1 q.2.2}) (h : ∀ (a₁ a₂ a₃ : α), p (e a₁) (e a₂) (e a₃)) (b₁ b₂ b₃ : β) :
p b₁ b₂ b₃
source
theorem DenseRange.equalizer {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] [TopologicalSpace γ] [T2Space γ] {f : α → β} (hfd : DenseRange 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.

source
theorem Filter.HasBasis.hasBasis_of_isDenseInducing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [RegularSpace β] {ι : Type u_5} {s : ι → Set α} {p : ι → Prop} {x : α} (h : (nhds x).HasBasis p s) {f : α → β} (hf : IsDenseInducing f) :
(nhds (f x)).HasBasis p fun (i : ι) => closure (f '' s i)