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

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.

theorem Dense.isDenseInducing_val {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : Dense s) : IsDenseInducing Subtype.val

theorem IsDenseInducing.isInducing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) : Topology.IsInducing i

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

theorem IsDenseInducing.continuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) : Continuous i

theorem IsDenseInducing.closure_range {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) : closure (Set.range i) = Set.univ

theorem IsDenseInducing.preconnectedSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [PreconnectedSpace α] (di : IsDenseInducing i) : PreconnectedSpace β

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)

theorem IsDenseInducing.dense_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) {s : Set α} : Dense (i '' s) ↔ Dense s

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.

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

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.

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→ β

theorem IsDenseInducing.nhdsWithin_neBot {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) (b : β) : (nhdsWithin b (Set.range i)).NeBot

theorem IsDenseInducing.comap_nhds_neBot {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) (b : β) : (Filter.comap i (nhds b)).NeBot

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

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

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)

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

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

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

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

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.

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

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

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

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)

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

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

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

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

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

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

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

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

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)

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.

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

theorem IsDenseEmbedding.isDenseInducing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : α → β} (de : IsDenseEmbedding e) : IsDenseInducing e

theorem IsDenseEmbedding.inj_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : α → β} (de : IsDenseEmbedding e) {x y : α} : e x = e y ↔ x = y

theorem IsDenseEmbedding.isEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : α → β} (de : IsDenseEmbedding e) : Topology.IsEmbedding e

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.

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.

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, ⋯⟩

@[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

theorem IsDenseEmbedding.subtype {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : α → β} (de : IsDenseEmbedding e) (p : α → Prop) : IsDenseEmbedding (subtypeEmb p e)

theorem IsDenseEmbedding.dense_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : α → β} (de : IsDenseEmbedding e) {s : Set α} : Dense (e '' s) ↔ Dense s

theorem IsDenseEmbedding.id {α : Type u_5} [TopologicalSpace α] : IsDenseEmbedding id

theorem Dense.isDenseEmbedding_val {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : Dense s) : IsDenseEmbedding Subtype.val

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

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₂

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₃

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₀

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₂

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₃

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.

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)