Documentation

Mathlib.Topology.DenseEmbedding

Dense embeddings #

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 IsDenseInducing (not necessarily injective).

structure IsDenseInducing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (i : αβ) extends Inducing :

i : α → β is "dense inducing" if it has dense range and the topology on α is the one induced by i from the topology on β.

Instances For
    theorem IsDenseInducing.dense {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : αβ} (self : IsDenseInducing i) :

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

    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) :
    theorem IsDenseInducing.closure_range {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : αβ} (di : IsDenseInducing i) :
    closure (Set.range i) = Set.univ
    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) :

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

    theorem IsDenseInducing.prod {α : 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 fun (p : α × γ) => (e₁ p.1, e₂ p.2)

    The product of two dense inducings is a dense inducing

    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) :
     γ -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
    Instances For
      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 : α), snhds a, tnhds (i a), ∀ (b : α), i b tb s) :
      structure IsDenseEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : αβ) extends IsDenseInducing :

      A dense embedding is an embedding with dense image.

      Instances For
        theorem IsDenseEmbedding.inj {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : αβ} (self : IsDenseEmbedding e) :

        A dense embedding is injective.

        theorem IsDenseEmbedding.mk' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : αβ) (c : Continuous e) (dense : DenseRange e) (inj : Function.Injective e) (H : ∀ (a : α), snhds a, tnhds (e a), ∀ (b : α), e b tb s) :
        @[deprecated IsDenseEmbedding.mk']
        theorem DenseEmbedding.mk' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : αβ) (c : Continuous e) (dense : DenseRange e) (inj : Function.Injective e) (H : ∀ (a : α), snhds a, tnhds (e a), ∀ (b : α), e b tb s) :

        Alias of IsDenseEmbedding.mk'.

        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.to_embedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : αβ} (de : IsDenseEmbedding e) :

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

        theorem IsDenseEmbedding.prod {α : 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.

        @[simp]
        theorem IsDenseEmbedding.subtypeEmb_coe {β : Type u_2} [TopologicalSpace β] {α : Type u_5} (p : αProp) (e : αβ) (x : { x : α // p x }) :
        (IsDenseEmbedding.subtypeEmb p e x) = e x
        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
        Instances For
          theorem IsDenseEmbedding.subtype {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : αβ} (de : IsDenseEmbedding e) (p : αProp) :
          theorem IsDenseEmbedding.dense_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : αβ} (de : IsDenseEmbedding e) {s : Set α} :
          Dense (e '' s) Dense s
          @[deprecated IsDenseEmbedding.id]

          Alias of IsDenseEmbedding.id.

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

          Alias of Dense.isDenseEmbedding_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 β] [T3Space β] {ι : 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)