Mathlib.Topology.DenseEmbedding

IsDenseInducing structure

[TopologicalSpace α] [TopologicalSpace β] (i : α → β) : Prop
    extends IsInducing i

Full source

/-- `i : α → β` is "dense inducing" if it has dense range and the topology on `α`
  is the one induced by `i` from the topology on `β`. -/
structure IsDenseInducing [TopologicalSpace α] [TopologicalSpace β] (i : α → β) : Prop
    extends IsInducing i where
  /-- The range of a dense inducing map is a dense set. -/
  protected dense : DenseRange i

Dense Inducing Function

Informal description

A function $ i : \alpha \to \beta $ between topological spaces is called *dense inducing* if it has dense range and the topology on $ \alpha $ is the one induced by $ i $ from the topology on $ \beta $.

Dense.isDenseInducing_val theorem

{s : Set α} (hs : Dense s) : IsDenseInducing (@Subtype.val α s)

Full source

theorem _root_.Dense.isDenseInducing_val {s : Set α} (hs : Dense s) :
    IsDenseInducing (@Subtype.val α s) := ⟨IsInducing.subtypeVal, hs.denseRange_val⟩

Inclusion Map of Dense Subset is Dense Inducing

Informal description

For any dense subset $s$ of a topological space $\alpha$, the inclusion map $\iota \colon s \to \alpha$ is dense inducing, meaning it has dense range and the subspace topology on $s$ is induced by $\iota$ from the topology on $\alpha$.

IsDenseInducing.isInducing theorem

(di : IsDenseInducing i) : IsInducing i

Full source

lemma isInducing (di : IsDenseInducing i) : IsInducing i := di.toIsInducing

Dense Inducing Implies Inducing Topology

Informal description

If a function $i \colon \alpha \to \beta$ between topological spaces is dense inducing, then it is also inducing, meaning that the topology on $\alpha$ is the one induced by $i$ from the topology on $\beta$.

IsDenseInducing.nhds_eq_comap theorem

(di : IsDenseInducing i) : ∀ a : α, 𝓝 a = comap i (𝓝 <| i a)

Full source

theorem nhds_eq_comap (di : IsDenseInducing i) : ∀ a : α, 𝓝 a = comap i (𝓝 <| i a) :=
  di.isInducing.nhds_eq_comap

Neighborhood Filter Characterization for Dense Inducing Maps

Informal description

For any dense inducing function $i \colon \alpha \to \beta$ between topological spaces and any point $a \in \alpha$, the neighborhood filter $\mathcal{N}_a$ of $a$ in $\alpha$ is equal to the preimage under $i$ of the neighborhood filter $\mathcal{N}_{i(a)}$ of $i(a)$ in $\beta$, i.e., $\mathcal{N}_a = i^{-1}(\mathcal{N}_{i(a)})$.

IsDenseInducing.continuous theorem

(di : IsDenseInducing i) : Continuous i

Full source

protected theorem continuous (di : IsDenseInducing i) : Continuous i :=
  di.isInducing.continuous

Continuity of Dense Inducing Maps

Informal description

If $i \colon \alpha \to \beta$ is a dense inducing function between topological spaces, then $i$ is continuous.

IsDenseInducing.closure_range theorem

(di : IsDenseInducing i) : closure (range i) = univ

Full source

theorem closure_range (di : IsDenseInducing i) : closure (range i) = univ :=
  di.dense.closure_range

Closure of Range Equals Codomain for Dense Inducing Functions

Informal description

For a dense inducing function $i : \alpha \to \beta$ between topological spaces, the closure of the range of $i$ is equal to the entire space $\beta$, i.e., $\overline{\text{range}(i)} = \beta$.

IsDenseInducing.preconnectedSpace theorem

[PreconnectedSpace α] (di : IsDenseInducing i) : PreconnectedSpace β

Full source

protected theorem preconnectedSpace [PreconnectedSpace α] (di : IsDenseInducing i) :
    PreconnectedSpace β :=
  di.dense.preconnectedSpace di.continuous

Dense Inducing Maps Preserve Preconnectedness

Informal description

If $\alpha$ is a preconnected topological space and $i \colon \alpha \to \beta$ is a dense inducing function, then $\beta$ is also preconnected.

IsDenseInducing.closure_image_mem_nhds theorem

{s : Set α} {a : α} (di : IsDenseInducing i) (hs : s ∈ 𝓝 a) : closure (i '' s) ∈ 𝓝 (i a)

Full source

theorem closure_image_mem_nhds {s : Set α} {a : α} (di : IsDenseInducing i) (hs : s ∈ 𝓝 a) :
    closureclosure (i '' s) ∈ 𝓝 (i a) := by
  rw [di.nhds_eq_comap a, ((nhds_basis_opens _).comap _).mem_iff] at hs
  rcases hs with ⟨U, ⟨haU, hUo⟩, sub : i ⁻¹' Ui ⁻¹' U ⊆ s⟩
  refine mem_of_superset (hUo.mem_nhds haU) ?_
  calc
    U ⊆ closure (i '' (i ⁻¹' U)) := di.dense.subset_closure_image_preimage_of_isOpen hUo
    _ ⊆ closure (i '' s) := closure_mono (image_subset i sub)

Closure of Image of Neighborhood under Dense Inducing Map is Neighborhood of Image Point

Informal description

Let $i \colon \alpha \to \beta$ be a dense inducing map between topological spaces, and let $s \subseteq \alpha$ be a neighborhood of a point $a \in \alpha$. Then the closure of the image $i(s)$ is a neighborhood of $i(a)$ in $\beta$.

IsDenseInducing.dense_image theorem

(di : IsDenseInducing i) {s : Set α} : Dense (i '' s) ↔ Dense s

Full source

theorem dense_image (di : IsDenseInducing i) {s : Set α} : DenseDense (i '' s) ↔ Dense s := by
  refine ⟨fun H x => ?_, di.dense.dense_image di.continuous⟩
  rw [di.isInducing.closure_eq_preimage_closure_image, H.closure_eq, preimage_univ]
  trivial

Density Preservation under Dense Inducing Maps

Informal description

Let $i \colon \alpha \to \beta$ be a dense inducing map between topological spaces. For any subset $s \subseteq \alpha$, the image $i(s)$ is dense in $\beta$ if and only if $s$ is dense in $\alpha$.

IsDenseInducing.interior_compact_eq_empty theorem

[T2Space β] (di : IsDenseInducing i) (hd : Dense (range i)ᶜ) {s : Set α} (hs : IsCompact s) : interior s = ∅

Full source

/-- If `i : α → β` is a dense embedding with dense complement of the range, then any compact set in
`α` has empty interior. -/
theorem interior_compact_eq_empty [T2Space β] (di : IsDenseInducing i) (hd : Dense (range i)ᶜ)
    {s : Set α} (hs : IsCompact s) : interior s = ∅ := by
  refine eq_empty_iff_forall_not_mem.2 fun x hx => ?_
  rw [mem_interior_iff_mem_nhds] at hx
  have := di.closure_image_mem_nhds hx
  rw [(hs.image di.continuous).isClosed.closure_eq] at this
  rcases hd.inter_nhds_nonempty this with ⟨y, hyi, hys⟩
  exact hyi (image_subset_range _ _ hys)

Compact Sets Have Empty Interior under Dense Inducing Maps with Dense Complement

Informal description

Let $i \colon \alpha \to \beta$ be a dense inducing map between topological spaces, where $\beta$ is Hausdorff. If the complement of the range of $i$ is dense in $\beta$, then any compact subset $s \subseteq \alpha$ has empty interior, i.e., $\text{interior}(s) = \emptyset$.

IsDenseInducing.prodMap theorem

 [TopologicalSpace γ] [TopologicalSpace δ] {e₁ : α → β} {e₂ : γ → δ} (de₁ : IsDenseInducing e₁)
  (de₂ : IsDenseInducing e₂) : IsDenseInducing (Prod.map e₁ e₂)

Full source

/-- The product of two dense inducings is a dense inducing -/
protected theorem prodMap [TopologicalSpace γ] [TopologicalSpace δ] {e₁ : α → β} {e₂ : γ → δ}
    (de₁ : IsDenseInducing e₁) (de₂ : IsDenseInducing e₂) :
    IsDenseInducing (Prod.map e₁ e₂) where
  toIsInducing := de₁.isInducing.prodMap de₂.isInducing
  dense := de₁.dense.prodMap de₂.dense

Product of Dense Inducing Maps is Dense Inducing

Informal description

Let $\alpha, \beta, \gamma, \delta$ be topological spaces, and let $e_1 \colon \alpha \to \beta$ and $e_2 \colon \gamma \to \delta$ be dense inducing maps. Then the product map $e_1 \times e_2 \colon \alpha \times \gamma \to \beta \times \delta$ is also dense inducing.

IsDenseInducing.separableSpace theorem

[SeparableSpace α] (di : IsDenseInducing i) : SeparableSpace β

Full source

/-- If the domain of a `IsDenseInducing` map is a separable space, then so is the codomain. -/
protected theorem separableSpace [SeparableSpace α] (di : IsDenseInducing i) : SeparableSpace β :=
  di.dense.separableSpace di.continuous

Separability is preserved under dense inducing maps

Informal description

Let $\alpha$ and $\beta$ be topological spaces, and let $i \colon \alpha \to \beta$ be a dense inducing map. If $\alpha$ is separable, then $\beta$ is also separable.

IsDenseInducing.tendsto_comap_nhds_nhds theorem

 {d : δ} {a : α} (di : IsDenseInducing i) (H : Tendsto h (𝓝 d) (𝓝 (i a))) (comm : h ∘ g = i ∘ f) :
  Tendsto f (comap g (𝓝 d)) (𝓝 a)

Full source

/--
```
 γ -f→ α
g↓     ↓e
 δ -h→ β
```
-/
theorem tendsto_comap_nhds_nhds {d : δ} {a : α} (di : IsDenseInducing i)
    (H : Tendsto h (𝓝 d) (𝓝 (i a))) (comm : h ∘ g = i ∘ f) : Tendsto f (comap g (𝓝 d)) (𝓝 a) := by
  have lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d := map_comap_le
  replace lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d) := map_mono lim1
  rw [Filter.map_map, comm, ← Filter.map_map, map_le_iff_le_comap] at lim1
  have lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a)) := comap_mono H
  rw [← di.nhds_eq_comap] at lim2
  exact le_trans lim1 lim2

Limit Preservation under Dense Inducing Maps via Commutative Diagram

Informal description

Consider the following commutative diagram of topological spaces and continuous maps: ``` γ -f→ α g↓ ↓i δ -h→ β ``` where $i \colon \alpha \to \beta$ is a dense inducing map. If $h$ tends to $i(a)$ as its input tends to $d$, then $f$ tends to $a$ as its input tends to any point in the preimage of $d$ under $g$.

IsDenseInducing.nhdsWithin_neBot theorem

(di : IsDenseInducing i) (b : β) : NeBot (𝓝[range i] b)

Full source

protected theorem nhdsWithin_neBot (di : IsDenseInducing i) (b : β) : NeBot (𝓝[range i] b) :=
  di.dense.nhdsWithin_neBot b

Non-triviality of Neighborhood Filter Within Range of Dense Inducing Function

Informal description

For any dense inducing function $ i \colon \alpha \to \beta $ between topological spaces and any point $ b \in \beta $, the neighborhood filter of $ b $ within the range of $ i $ is non-trivial. That is, $ \mathcal{N}_{\text{range } i}(b) $ is not the trivial filter.

IsDenseInducing.comap_nhds_neBot theorem

(di : IsDenseInducing i) (b : β) : NeBot (comap i (𝓝 b))

Full source

theorem comap_nhds_neBot (di : IsDenseInducing i) (b : β) : NeBot (comap i (𝓝 b)) :=
  comap_neBot fun s hs => by
    rcases mem_closure_iff_nhds.1 (di.dense b) s hs with ⟨_, ⟨ha, a, rfl⟩⟩
    exact ⟨a, ha⟩

Non-triviality of Preimage Neighborhood Filter under Dense Inducing Function

Informal description

For any dense inducing function $ i \colon \alpha \to \beta $ between topological spaces and any point $ b \in \beta $, the preimage filter of the neighborhood filter of $ b $ under $ i $ is non-trivial. That is, the filter $ i^{-1}(\mathcal{N}(b)) $ does not contain the empty set.

IsDenseInducing.extend definition

(di : IsDenseInducing i) (f : α → γ) (b : β) : γ

Full source

/-- 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`. -/
def extend (di : IsDenseInducing i) (f : α → γ) (b : β) : γ :=
  @limUnder _ _ _ ⟨f (di.dense.some b)⟩ (comap i (𝓝 b)) f

Extension of a function along a dense inducing map

Informal description

Given a dense inducing function $ i : \alpha \to \beta $ between topological spaces and a function $ f : \alpha \to \gamma $, the function `IsDenseInducing.extend di f` constructs an extension $ g : \beta \to \gamma $ of $ f $ along $ i $. Specifically, for each $ b \in \beta $, $ g(b) $ is defined as the limit of $ f $ under the filter `comap i (𝓝 b)`. If $ \gamma $ 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 $.

IsDenseInducing.extend_eq_of_tendsto theorem

 [T2Space γ] (di : IsDenseInducing i) {b : β} {c : γ} {f : α → γ} (hf : Tendsto f (comap i (𝓝 b)) (𝓝 c)) :
  di.extend f b = c

Full source

theorem extend_eq_of_tendsto [T2Space γ] (di : IsDenseInducing i) {b : β} {c : γ} {f : α → γ}
    (hf : Tendsto f (comap i (𝓝 b)) (𝓝 c)) : di.extend f b = c :=
  haveI := di.comap_nhds_neBot
  hf.limUnder_eq

Extension of a Function Along a Dense Inducing Map Preserves Limits in Hausdorff Spaces

Informal description

Let $ \gamma $ be a Hausdorff space, $ i : \alpha \to \beta $ a dense inducing map between topological spaces, and $ f : \alpha \to \gamma $ a function. For any point $ b \in \beta $ and $ c \in \gamma $, if $ f $ tends to $ c $ along the preimage filter of the neighborhood filter of $ b $ under $ i $, then the extension $ \text{di.extend}\, f $ of $ f $ along $ i $ satisfies $ \text{di.extend}\, f\, b = c $.

IsDenseInducing.extend_eq_at theorem

[T2Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (hf : ContinuousAt f a) : di.extend f (i a) = f a

Full source

theorem extend_eq_at [T2Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α}
    (hf : ContinuousAt f a) : di.extend f (i a) = f a :=
  extend_eq_of_tendsto _ <| di.nhds_eq_comap a ▸ hf

Extension of Continuous Function Along Dense Inducing Map Preserves Value at Point

Informal description

Let $i \colon \alpha \to \beta$ be a dense inducing map between topological spaces, and let $\gamma$ be a Hausdorff space. For any function $f \colon \alpha \to \gamma$ that is continuous at a point $a \in \alpha$, the extension of $f$ along $i$ satisfies $(\text{di.extend}\, f)(i(a)) = f(a)$.

IsDenseInducing.extend_eq_at' theorem

 [T2Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (c : γ) (hf : Tendsto f (𝓝 a) (𝓝 c)) : di.extend f (i a) = f a

Full source

theorem extend_eq_at' [T2Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (c : γ)
    (hf : Tendsto f (𝓝 a) (𝓝 c)) : di.extend f (i a) = f a :=
  di.extend_eq_at (continuousAt_of_tendsto_nhds hf)

Extension of Function Along Dense Inducing Map Preserves Limit Points

Informal description

Let $\gamma$ be a Hausdorff space, $i \colon \alpha \to \beta$ a dense inducing map between topological spaces, and $f \colon \alpha \to \gamma$ a function. For any point $a \in \alpha$ and $c \in \gamma$, if $f$ tends to $c$ at $a$ (i.e., $\lim_{x \to a} f(x) = c$), then the extension of $f$ along $i$ satisfies $(\text{di.extend}\, f)(i(a)) = f(a)$.

IsDenseInducing.extend_eq theorem

[T2Space γ] (di : IsDenseInducing i) {f : α → γ} (hf : Continuous f) (a : α) : di.extend f (i a) = f a

Full source

theorem extend_eq [T2Space γ] (di : IsDenseInducing i) {f : α → γ} (hf : Continuous f) (a : α) :
    di.extend f (i a) = f a :=
  di.extend_eq_at hf.continuousAt

Extension of Continuous Function Along Dense Inducing Map Preserves Values

Informal description

Let $i \colon \alpha \to \beta$ be a dense inducing map between topological spaces, and let $\gamma$ be a Hausdorff space. For any continuous function $f \colon \alpha \to \gamma$, the extension of $f$ along $i$ satisfies $(\text{di.extend}\, f)(i(a)) = f(a)$ for all $a \in \alpha$.

IsDenseInducing.extend_eq' theorem

 [T2Space γ] {f : α → γ} (di : IsDenseInducing i) (hf : ∀ b, ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)) (a : α) :
  di.extend f (i a) = f a

Full source

/-- 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 extend_eq' [T2Space γ] {f : α → γ} (di : IsDenseInducing i)
    (hf : ∀ b, ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)) (a : α) : di.extend f (i a) = f a := by
  rcases hf (i a) with ⟨b, hb⟩
  refine di.extend_eq_at' b ?_
  rwa [← di.isInducing.nhds_eq_comap] at hb

Extension of Function Along Dense Inducing Map Preserves Values Under Limit Condition

Informal description

Let $\gamma$ be a Hausdorff space, $i \colon \alpha \to \beta$ a dense inducing map between topological spaces, and $f \colon \alpha \to \gamma$ a function. Suppose that for every $b \in \beta$, there exists $c \in \gamma$ such that $f$ tends to $c$ along the filter $\text{comap}\, i\, (\mathcal{N}(b))$. Then the extension of $f$ along $i$ satisfies $(\text{di.extend}\, f)(i(a)) = f(a)$ for all $a \in \alpha$.

IsDenseInducing.extend_unique_at theorem

 [T2Space γ] {b : β} {f : α → γ} {g : β → γ} (di : IsDenseInducing i) (hf : ∀ᶠ x in comap i (𝓝 b), g (i x) = f x)
  (hg : ContinuousAt g b) : di.extend f b = g b

Full source

theorem extend_unique_at [T2Space γ] {b : β} {f : α → γ} {g : β → γ} (di : IsDenseInducing i)
    (hf : ∀ᶠ x in comap i (𝓝 b), g (i x) = f x) (hg : ContinuousAt g b) : di.extend f b = g b := by
  refine di.extend_eq_of_tendsto fun s hs => mem_map.2 ?_
  suffices ∀ᶠ x : α in comap i (𝓝 b), g (i x) ∈ s from
    hf.mp (this.mono fun x hgx hfx => hfx ▸ hgx)
  clear hf f
  refine eventually_comap.2 ((hg.eventually hs).mono ?_)
  rintro _ hxs x rfl
  exact hxs

Uniqueness of Continuous Extension at a Point for Dense Inducing Maps in Hausdorff Spaces

Informal description

Let $ \gamma $ be a Hausdorff space, $ i : \alpha \to \beta $ a dense inducing map between topological spaces, and $ f : \alpha \to \gamma $ a function. Suppose $ g : \beta \to \gamma $ is a function that is continuous at $ b \in \beta $ and satisfies $ g(i(x)) = f(x) $ for all $ x $ in a neighborhood of $ b $ under the preimage filter $ \text{comap}\, i\, (\mathcal{N}(b)) $. Then the extension $ \text{di.extend}\, f $ of $ f $ along $ i $ satisfies $ \text{di.extend}\, f\, b = g(b) $.

IsDenseInducing.extend_unique theorem

 [T2Space γ] {f : α → γ} {g : β → γ} (di : IsDenseInducing i) (hf : ∀ x, g (i x) = f x) (hg : Continuous g) :
  di.extend f = g

Full source

theorem extend_unique [T2Space γ] {f : α → γ} {g : β → γ} (di : IsDenseInducing i)
    (hf : ∀ x, g (i x) = f x) (hg : Continuous g) : di.extend f = g :=
  funext fun _ => extend_unique_at di (Eventually.of_forall hf) hg.continuousAt

Uniqueness of Continuous Extension for Dense Inducing Maps in Hausdorff Spaces

Informal description

Let $\gamma$ be a Hausdorff space, $i : \alpha \to \beta$ a dense inducing map between topological spaces, and $f : \alpha \to \gamma$ a function. If $g : \beta \to \gamma$ is a continuous function such that $g(i(x)) = f(x)$ for all $x \in \alpha$, then the extension $\text{di.extend}\, f$ of $f$ along $i$ satisfies $\text{di.extend}\, f = g$.

IsDenseInducing.continuousAt_extend theorem

 [T3Space γ] {b : β} {f : α → γ} (di : IsDenseInducing i) (hf : ∀ᶠ x in 𝓝 b, ∃ c, Tendsto f (comap i <| 𝓝 x) (𝓝 c)) :
  ContinuousAt (di.extend f) b

Full source

theorem continuousAt_extend [T3Space γ] {b : β} {f : α → γ} (di : IsDenseInducing i)
    (hf : ∀ᶠ x in 𝓝 b, ∃ c, Tendsto f (comap i <| 𝓝 x) (𝓝 c)) : ContinuousAt (di.extend f) b := by
  set φ := di.extend f
  haveI := di.comap_nhds_neBot
  suffices ∀ V' ∈ 𝓝 (φ b), IsClosed V' → φ ⁻¹' V' ∈ 𝓝 b by
    simpa [ContinuousAt, (closed_nhds_basis (φ b)).tendsto_right_iff]
  intro V' V'_in V'_closed
  set V₁ := { x | Tendsto f (comap i <| 𝓝 x) (𝓝 <| φ x) }
  have V₁_in : V₁ ∈ 𝓝 b := by
    filter_upwards [hf]
    rintro x ⟨c, hc⟩
    rwa [← di.extend_eq_of_tendsto hc] at hc
  obtain ⟨V₂, V₂_in, V₂_op, hV₂⟩ : ∃ V₂ ∈ 𝓝 b, IsOpen V₂ ∧ ∀ x ∈ i ⁻¹' V₂, f x ∈ V' := by
    simpa [and_assoc] using
      ((nhds_basis_opens' b).comap i).tendsto_left_iff.mp (mem_of_mem_nhds V₁_in : b ∈ V₁) V' V'_in
  suffices ∀ x ∈ V₁ ∩ V₂, φ x ∈ V' by filter_upwards [inter_mem V₁_in V₂_in] using this
  rintro x ⟨x_in₁, x_in₂⟩
  have hV₂x : V₂ ∈ 𝓝 x := IsOpen.mem_nhds V₂_op x_in₂
  apply V'_closed.mem_of_tendsto x_in₁
  use V₂
  tauto

Continuity of Function Extension Along Dense Inducing Map at a Point in T₃ Spaces

Informal description

Let $X$ and $Y$ be topological spaces, $i : X \to Y$ a dense inducing map, and $\gamma$ a T₃ space. Given a function $f : X \to \gamma$ and a point $b \in Y$, suppose that for all $x$ in some neighborhood of $b$, there exists $c \in \gamma$ such that $f$ tends to $c$ along the preimage filter of the neighborhood filter of $x$ under $i$. Then the extension $\text{di.extend}\, f$ of $f$ along $i$ is continuous at $b$.

IsDenseInducing.continuous_extend theorem

 [T3Space γ] {f : α → γ} (di : IsDenseInducing i) (hf : ∀ b, ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)) :
  Continuous (di.extend f)

Full source

theorem continuous_extend [T3Space γ] {f : α → γ} (di : IsDenseInducing i)
    (hf : ∀ b, ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)) : Continuous (di.extend f) :=
  continuous_iff_continuousAt.mpr fun _ => di.continuousAt_extend <| univ_mem' hf

Continuous Extension Theorem for Dense Inducing Maps in T₃ Spaces

Informal description

Let $X$ and $Y$ be topological spaces, $i : X \to Y$ a dense inducing map, and $\gamma$ a T₃ space. Given a function $f : X \to \gamma$ such that for every $b \in Y$, there exists $c \in \gamma$ for which $f$ tends to $c$ along the preimage filter of the neighborhood filter of $b$ under $i$, then the extension $\text{di.extend}\, f$ of $f$ along $i$ is continuous.

IsDenseInducing.mk' theorem

 (i : α → β) (c : Continuous i) (dense : ∀ x, x ∈ closure (range i))
  (H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (i a), ∀ b, i b ∈ t → b ∈ s) : IsDenseInducing i

Full source

theorem mk' (i : α → β) (c : Continuous i) (dense : ∀ x, x ∈ closure (range i))
    (H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (i a), ∀ b, i b ∈ t → b ∈ s) : IsDenseInducing i where
  toIsInducing := isInducing_iff_nhds.2 fun a =>
      le_antisymm (c.tendsto _).le_comap (by simpa [Filter.le_def] using H a)
  dense := dense

Characterization of Dense Inducing Maps via Neighborhood Conditions

Informal description

Let $i \colon \alpha \to \beta$ be a continuous function between topological spaces such that: 1. The range of $i$ is dense in $\beta$, i.e., $\overline{\mathrm{range}(i)} = \beta$. 2. For every point $a \in \alpha$ and every neighborhood $s$ of $a$, there exists a neighborhood $t$ of $i(a)$ in $\beta$ such that for all $b \in \alpha$, if $i(b) \in t$ then $b \in s$. Then $i$ is a dense inducing map.

Dense.extend definition

(hs : Dense s) (f : s → β) : α → β

Full source

/-- 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. -/
noncomputable def extend (hs : Dense s) (f : s → β) : α → β :=
    hs.isDenseInducing_val.extend f

Extension of a function from a dense subset

Informal description

Given a dense subset $s$ of a topological space $\alpha$ and a function $f \colon s \to \beta$, the function `Dense.extend hs f` constructs an extension of $f$ to a function $\alpha \to \beta$ by leveraging the fact that the inclusion map $\iota \colon s \to \alpha$ is dense inducing. Specifically, for each $a \in \alpha$, the value of the extension at $a$ is defined as the limit of $f$ under the filter `comap ι (𝓝 a)`. If $\beta$ is Hausdorff and $f$ has a continuous extension, then this is the unique such extension.

Dense.extend_eq_of_tendsto theorem

[T2Space β] (hs : Dense s) {a : α} {b : β} (hf : Tendsto f (comap (↑) (𝓝 a)) (𝓝 b)) : hs.extend f a = b

Full source

theorem extend_eq_of_tendsto [T2Space β] (hs : Dense s) {a : α} {b : β}
    (hf : Tendsto f (comap (↑) (𝓝 a)) (𝓝 b)) : hs.extend f a = b :=
  hs.isDenseInducing_val.extend_eq_of_tendsto hf

Extension of a Function from a Dense Subset Preserves Limits in Hausdorff Spaces

Informal description

Let $s$ be a dense subset of a topological space $\alpha$, and let $\beta$ be a Hausdorff space. Given a function $f \colon s \to \beta$ and a point $a \in \alpha$, if $f$ tends to $b \in \beta$ along the preimage filter of the neighborhood filter of $a$ under the inclusion map $\iota \colon s \to \alpha$, then the extension $\text{hs.extend}\, f$ of $f$ to $\alpha$ satisfies $\text{hs.extend}\, f\, a = b$.

Dense.extend_eq_at theorem

[T2Space β] (hs : Dense s) {f : s → β} {x : s} (hf : ContinuousAt f x) : hs.extend f x = f x

Full source

theorem extend_eq_at [T2Space β] (hs : Dense s) {f : s → β} {x : s}
    (hf : ContinuousAt f x) : hs.extend f x = f x :=
  hs.isDenseInducing_val.extend_eq_at hf

Extension of Continuous Function Preserves Value at Point in Dense Subset

Informal description

Let $s$ be a dense subset of a topological space $\alpha$, and let $\beta$ be a Hausdorff space. Given a function $f \colon s \to \beta$ that is continuous at a point $x \in s$, the extension of $f$ to $\alpha$ via `hs.extend f` satisfies `hs.extend f x = f x`.

Dense.extend_eq theorem

[T2Space β] (hs : Dense s) (hf : Continuous f) (x : s) : hs.extend f x = f x

Full source

theorem extend_eq [T2Space β] (hs : Dense s) (hf : Continuous f) (x : s) :
    hs.extend f x = f x :=
  hs.extend_eq_at hf.continuousAt

Extension of Continuous Function Preserves Values on Dense Subset in Hausdorff Spaces

Informal description

Let $s$ be a dense subset of a topological space $\alpha$, and let $\beta$ be a Hausdorff space. Given a continuous function $f \colon s \to \beta$, the extension of $f$ to $\alpha$ via `hs.extend f` satisfies `hs.extend f x = f x` for every $x \in s$.

Dense.extend_unique_at theorem

 [T2Space β] {a : α} {g : α → β} (hs : Dense s) (hf : ∀ᶠ x : s in comap (↑) (𝓝 a), g x = f x) (hg : ContinuousAt g a) :
  hs.extend f a = g a

Full source

theorem extend_unique_at [T2Space β] {a : α} {g : α → β} (hs : Dense s)
    (hf : ∀ᶠ x : s in comap (↑) (𝓝 a), g x = f x) (hg : ContinuousAt g a) :
    hs.extend f a = g a :=
  hs.isDenseInducing_val.extend_unique_at hf hg

Uniqueness of Continuous Extension at a Point for Dense Subsets in Hausdorff Spaces

Informal description

Let $\beta$ be a Hausdorff space, $s$ a dense subset of a topological space $\alpha$, and $f \colon s \to \beta$ a function. Suppose $g \colon \alpha \to \beta$ is a function that is continuous at a point $a \in \alpha$ and satisfies $g(x) = f(x)$ for all $x$ in a neighborhood of $a$ (with respect to the subspace topology on $s$). Then the extension of $f$ to $\alpha$ via the dense subset $s$ satisfies $\text{extend}_s f(a) = g(a)$.

Dense.extend_unique theorem

[T2Space β] {g : α → β} (hs : Dense s) (hf : ∀ x : s, g x = f x) (hg : Continuous g) : hs.extend f = g

Full source

theorem extend_unique [T2Space β] {g : α → β} (hs : Dense s)
    (hf : ∀ x : s, g x = f x) (hg : Continuous g) : hs.extend f = g :=
  hs.isDenseInducing_val.extend_unique hf hg

Uniqueness of Continuous Extension Along Dense Subset in Hausdorff Spaces

Informal description

Let $\beta$ be a Hausdorff space, $s$ a dense subset of a topological space $\alpha$, and $f \colon s \to \beta$ a function. If $g \colon \alpha \to \beta$ is a continuous function such that $g(x) = f(x)$ for all $x \in s$, then the extension $\text{hs.extend}\, f$ of $f$ along $s$ satisfies $\text{hs.extend}\, f = g$.

Dense.continuousAt_extend theorem

 [T3Space β] {a : α} (hs : Dense s) (hf : ∀ᶠ x in 𝓝 a, ∃ b, Tendsto f (comap (↑) <| 𝓝 x) (𝓝 b)) :
  ContinuousAt (hs.extend f) a

Full source

theorem continuousAt_extend [T3Space β] {a : α} (hs : Dense s)
    (hf : ∀ᶠ x in 𝓝 a, ∃ b, Tendsto f (comap (↑) <| 𝓝 x) (𝓝 b)) :
    ContinuousAt (hs.extend f) a :=
  hs.isDenseInducing_val.continuousAt_extend hf

Continuity of Function Extension Along Dense Subset at a Point in T₃ Spaces

Informal description

Let $X$ be a topological space with a dense subset $s \subseteq X$, and let $\beta$ be a T₃ space. Given a function $f \colon s \to \beta$ and a point $a \in X$, suppose that for all $x$ in some neighborhood of $a$, there exists $b \in \beta$ such that $f$ tends to $b$ along the preimage filter of the neighborhood filter of $x$ under the inclusion map $\iota \colon s \to X$. Then the extension $\text{hs.extend}\, f$ of $f$ along $s$ is continuous at $a$.

Dense.continuous_extend theorem

 [T3Space β] (hs : Dense s) (hf : ∀ a : α, ∃ b, Tendsto f (comap (↑) (𝓝 a)) (𝓝 b)) : Continuous (hs.extend f)

Full source

theorem continuous_extend [T3Space β] (hs : Dense s)
    (hf : ∀ a : α, ∃ b, Tendsto f (comap (↑) (𝓝 a)) (𝓝 b)) : Continuous (hs.extend f) :=
  hs.isDenseInducing_val.continuous_extend hf

Continuous Extension Theorem for Functions on Dense Subsets in T₃ Spaces

Informal description

Let $X$ be a topological space with a dense subset $s \subseteq X$, and let $\beta$ be a T₃ space. Given a function $f \colon s \to \beta$ such that for every point $a \in X$, there exists $b \in \beta$ for which $f$ tends to $b$ along the preimage filter of the neighborhood filter of $a$ under the inclusion map $\iota \colon s \to X$, then the extension $\text{hs.extend}\, f$ of $f$ along $s$ is continuous.

IsDenseEmbedding structure

[TopologicalSpace α] [TopologicalSpace β] (e : α → β) : Prop
    extends IsDenseInducing e

Full source

/-- A dense embedding is an embedding with dense image. -/
structure IsDenseEmbedding [TopologicalSpace α] [TopologicalSpace β] (e : α → β) : Prop
    extends IsDenseInducing e where
  /-- A dense embedding is injective. -/
  injective : Function.Injective e

Dense Embedding

Informal description

A function $ e : \alpha \to \beta $ between topological spaces is called a *dense embedding* if it satisfies the following properties: 1. **Dense image**: The image of $ e $ is dense in $ \beta $. 2. **Embedding**: The function $ e $ is injective and induces the topology on its codomain $ \beta $, meaning that the topology on $ \beta $ is the coarsest topology for which $ e $ is continuous. 3. **Continuity**: The function $ e $ is continuous. In other words, a dense embedding is an injective continuous map with dense image that also induces the topology on its codomain.

IsDenseEmbedding.mk' theorem

 [TopologicalSpace α] [TopologicalSpace β] (e : α → β) (c : Continuous e) (dense : DenseRange e)
  (injective : Function.Injective e) (H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (e a), ∀ b, e b ∈ t → b ∈ s) :
  IsDenseEmbedding e

Full source

lemma IsDenseEmbedding.mk' [TopologicalSpace α] [TopologicalSpace β] (e : α → β) (c : Continuous e)
    (dense : DenseRange e) (injective : Function.Injective e)
    (H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (e a), ∀ b, e b ∈ t → b ∈ s) : IsDenseEmbedding e :=
  { IsDenseInducing.mk' e c dense H with injective }

Characterization of Dense Embeddings via Neighborhood Conditions

Informal description

Let $\alpha$ and $\beta$ be topological spaces, and let $e \colon \alpha \to \beta$ be a function. Suppose that: 1. $e$ is continuous, 2. The range of $e$ is dense in $\beta$, 3. $e$ is injective, and 4. For every point $a \in \alpha$ and every neighborhood $s$ of $a$, there exists a neighborhood $t$ of $e(a)$ in $\beta$ such that for all $b \in \alpha$, if $e(b) \in t$ then $b \in s$. Then $e$ is a dense embedding, i.e., it is an injective continuous map with dense image that induces the topology on $\beta$.

IsDenseEmbedding.isDenseInducing theorem

(de : IsDenseEmbedding e) : IsDenseInducing e

Full source

lemma isDenseInducing (de : IsDenseEmbedding e) : IsDenseInducing e := de.toIsDenseInducing

Dense Embedding Implies Dense Inducing

Informal description

If $e \colon \alpha \to \beta$ is a dense embedding between topological spaces, then $e$ is also a dense inducing map.

IsDenseEmbedding.inj_iff theorem

(de : IsDenseEmbedding e) {x y} : e x = e y ↔ x = y

Full source

theorem inj_iff (de : IsDenseEmbedding e) {x y} : e x = e y ↔ x = y :=
  de.injective.eq_iff

Injectivity Criterion for Dense Embeddings

Informal description

For any dense embedding $e \colon \alpha \to \beta$ between topological spaces and any elements $x, y \in \alpha$, we have $e(x) = e(y)$ if and only if $x = y$.

IsDenseEmbedding.isEmbedding theorem

(de : IsDenseEmbedding e) : IsEmbedding e

Full source

theorem isEmbedding (de : IsDenseEmbedding e) : IsEmbedding e where __ := de

Dense Embedding Implies Embedding

Informal description

If $e \colon \alpha \to \beta$ is a dense embedding between topological spaces, then $e$ is an embedding (i.e., it is injective and induces the topology on its codomain $\beta$).

IsDenseEmbedding.separableSpace theorem

[SeparableSpace α] (de : IsDenseEmbedding e) : SeparableSpace β

Full source

/-- If the domain of a `IsDenseEmbedding` is a separable space, then so is its codomain. -/
protected theorem separableSpace [SeparableSpace α] (de : IsDenseEmbedding e) : SeparableSpace β :=
  de.isDenseInducing.separableSpace

Separability is preserved under dense embeddings

Informal description

Let $e \colon \alpha \to \beta$ be a dense embedding between topological spaces. If $\alpha$ is separable, then $\beta$ is also separable.

IsDenseEmbedding.prodMap theorem

 {e₁ : α → β} {e₂ : γ → δ} (de₁ : IsDenseEmbedding e₁) (de₂ : IsDenseEmbedding e₂) :
  IsDenseEmbedding fun p : α × γ => (e₁ p.1, e₂ p.2)

Full source

/-- The product of two dense embeddings is a dense embedding. -/
protected theorem prodMap {e₁ : α → β} {e₂ : γ → δ} (de₁ : IsDenseEmbedding e₁)
    (de₂ : IsDenseEmbedding e₂) : IsDenseEmbedding fun p : α × γ => (e₁ p.1, e₂ p.2) where
  toIsDenseInducing := de₁.isDenseInducing.prodMap de₂.isDenseInducing
  injective := de₁.injective.prodMap de₂.injective

Product of Dense Embeddings is a Dense Embedding

Informal description

Let $\alpha, \beta, \gamma, \delta$ be topological spaces, and let $e_1 \colon \alpha \to \beta$ and $e_2 \colon \gamma \to \delta$ be dense embeddings. Then the product map $e_1 \times e_2 \colon \alpha \times \gamma \to \beta \times \delta$ defined by $(e_1 \times e_2)(a, b) = (e_1(a), e_2(b))$ is also a dense embedding.

IsDenseEmbedding.subtypeEmb definition

{α : Type*} (p : α → Prop) (e : α → β) (x : { x // p x }) : { x // x ∈ closure (e '' {x | p x}) }

Full source

/-- The dense embedding of a subtype inside its closure. -/
@[simps]
def subtypeEmb {α : Type*} (p : α → Prop) (e : α → β) (x : { x // p x }) :
    { x // x ∈ closure (e '' { x | p x }) } :=
  ⟨e x, subset_closure <| mem_image_of_mem e x.prop⟩

Embedding of a subtype into the closure of its image

Informal description

Given a predicate $p : \alpha \to \text{Prop}$ and a function $e : \alpha \to \beta$, the function `subtypeEmb p e` maps an element $x$ of the subtype $\{x \mid p x\}$ to the element $e x$ in the closure of the image of $\{x \mid p x\}$ under $e$. In other words, for any $x$ in the subtype defined by $p$, the value $e x$ lies within the closure of the image of the set $\{x \mid p x\}$ under the function $e$.

IsDenseEmbedding.subtype theorem

(de : IsDenseEmbedding e) (p : α → Prop) : IsDenseEmbedding (subtypeEmb p e)

Full source

protected theorem subtype (de : IsDenseEmbedding e) (p : α → Prop) :
    IsDenseEmbedding (subtypeEmb p e) where
  dense :=
    dense_iff_closure_eq.2 <| by
      ext ⟨x, hx⟩
      rw [image_eq_range] at hx
      simpa [closure_subtype, ← range_comp, (· ∘ ·)]
  injective := (de.injective.comp Subtype.coe_injective).codRestrict _
  eq_induced :=
    (induced_iff_nhds_eq _).2 fun ⟨x, hx⟩ => by
      simp [subtypeEmb, nhds_subtype_eq_comap, de.isInducing.nhds_eq_comap, comap_comap,
        Function.comp_def]

Dense Embedding Property Preserved under Subtype Restriction

Informal description

Let $e \colon \alpha \to \beta$ be a dense embedding between topological spaces, and let $p \colon \alpha \to \text{Prop}$ be a predicate on $\alpha$. Then the function $\text{subtypeEmb}\, p\, e \colon \{x \mid p(x)\} \to \beta$, which maps $x$ to $e(x)$, is also a dense embedding.

IsDenseEmbedding.dense_image theorem

(de : IsDenseEmbedding e) {s : Set α} : Dense (e '' s) ↔ Dense s

Full source

theorem dense_image (de : IsDenseEmbedding e) {s : Set α} : DenseDense (e '' s) ↔ Dense s :=
  de.isDenseInducing.dense_image

Density Preservation under Dense Embeddings

Informal description

Let $e \colon \alpha \to \beta$ be a dense embedding between topological spaces. For any subset $s \subseteq \alpha$, the image $e(s)$ is dense in $\beta$ if and only if $s$ is dense in $\alpha$.

IsDenseEmbedding.id theorem

{α : Type*} [TopologicalSpace α] : IsDenseEmbedding (id : α → α)

Full source

protected lemma id {α : Type*} [TopologicalSpace α] : IsDenseEmbedding (id : α → α) :=
  { IsEmbedding.id with dense := denseRange_id }

Identity Function is a Dense Embedding

Informal description

For any topological space $\alpha$, the identity function $\mathrm{id} \colon \alpha \to \alpha$ is a dense embedding. That is, it is injective, continuous, has dense image, and induces the topology on $\alpha$.

Dense.isDenseEmbedding_val theorem

[TopologicalSpace α] {s : Set α} (hs : Dense s) : IsDenseEmbedding ((↑) : s → α)

Full source

theorem Dense.isDenseEmbedding_val [TopologicalSpace α] {s : Set α} (hs : Dense s) :
    IsDenseEmbedding ((↑) : s → α) :=
  { IsEmbedding.subtypeVal with dense := hs.denseRange_val }

Dense Subset Inclusion is a Dense Embedding

Informal description

For any topological space $\alpha$ and a dense subset $s \subseteq \alpha$, the inclusion map $\iota: s \to \alpha$ is a dense embedding. That is, $\iota$ is injective, continuous, has dense image, and induces the topology on $\alpha$.

isClosed_property theorem

 [TopologicalSpace β] {e : α → β} {p : β → Prop} (he : DenseRange e) (hp : IsClosed {x | p x}) (h : ∀ a, p (e a)) :
  ∀ b, p b

Full source

theorem isClosed_property [TopologicalSpace β] {e : α → β} {p : β → Prop} (he : DenseRange e)
    (hp : IsClosed { x | p x }) (h : ∀ a, p (e a)) : ∀ b, p b := by
  have : univuniv ⊆ { b | p b } :=
    calc
      univ = closure (range e) := he.closure_range.symm
      _ ⊆ closure { b | p b } := closure_mono <| range_subset_iff.mpr h
      _ = _ := hp.closure_eq
  simpa only [univ_subset_iff, eq_univ_iff_forall, mem_setOf]

Dense Range Implies Property Holds Everywhere for Closed Predicates

Informal description

Let $\alpha$ and $\beta$ be topological spaces, and let $e \colon \alpha \to \beta$ be a function with dense range. If $\{x \in \beta \mid p(x)\}$ is a closed subset of $\beta$ and $p(e(a))$ holds for every $a \in \alpha$, then $p(b)$ holds for every $b \in \beta$.

isClosed_property2 theorem

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

Full source

theorem isClosed_property2 [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₂ :=
  have : ∀ q : β × β, p q.1 q.2 := isClosed_property (he.prodMap he) hp fun _ => h _ _
  fun b₁ b₂ => this ⟨b₁, b₂⟩

Dense Range Implies Binary Property Holds Everywhere for Closed Predicates

Informal description

Let $\alpha$ and $\beta$ be topological spaces, and let $e \colon \alpha \to \beta$ be a function with dense range. If the set $\{(x, y) \in \beta \times \beta \mid p(x, y)\}$ is closed in $\beta \times \beta$ and $p(e(a_1), e(a_2))$ holds for every $a_1, a_2 \in \alpha$, then $p(b_1, b_2)$ holds for every $b_1, b_2 \in \beta$.

isClosed_property3 theorem

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

Full source

theorem isClosed_property3 [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₃ :=
  have : ∀ q : β × β × β, p q.1 q.2.1 q.2.2 :=
    isClosed_property (he.prodMap <| he.prodMap he) hp fun _ => h _ _ _
  fun b₁ b₂ b₃ => this ⟨b₁, b₂, b₃⟩

Dense Range Implies Ternary Property Holds Everywhere for Closed Predicates

Informal description

Let $\alpha$ and $\beta$ be topological spaces, and let $e \colon \alpha \to \beta$ be a function with dense range. If the set $\{(x, y, z) \in \beta \times \beta \times \beta \mid p(x, y, z)\}$ is closed in $\beta \times \beta \times \beta$ and $p(e(a_1), e(a_2), e(a_3))$ holds for all $a_1, a_2, a_3 \in \alpha$, then $p(b_1, b_2, b_3)$ holds for all $b_1, b_2, b_3 \in \beta$.

DenseRange.induction_on theorem

 [TopologicalSpace β] {e : α → β} (he : DenseRange e) {p : β → Prop} (b₀ : β) (hp : IsClosed {b | p b})
  (ih : ∀ a : α, p <| e a) : p b₀

Full source

@[elab_as_elim]
theorem DenseRange.induction_on [TopologicalSpace β] {e : α → β} (he : DenseRange e) {p : β → Prop}
    (b₀ : β) (hp : IsClosed { b | p b }) (ih : ∀ a : α, p <| e a) : p b₀ :=
  isClosed_property he hp ih b₀

Induction Principle for Dense Range Functions on Closed Predicates

Informal description

Let $\alpha$ and $\beta$ be topological spaces, and let $e \colon \alpha \to \beta$ be a function with dense range. For any predicate $p \colon \beta \to \text{Prop}$ such that the set $\{b \in \beta \mid p(b)\}$ is closed in $\beta$, if $p(e(a))$ holds for every $a \in \alpha$, then $p(b_0)$ holds for any given $b_0 \in \beta$.

DenseRange.induction_on₂ theorem

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

Full source

@[elab_as_elim]
theorem DenseRange.induction_on₂ [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₂ :=
  isClosed_property2 he hp h _ _

Dense Range Induction Principle for Binary Predicates on Closed Sets

Informal description

Let $\alpha$ and $\beta$ be topological spaces, and let $e \colon \alpha \to \beta$ be a function with dense range. For any binary predicate $p \colon \beta \times \beta \to \text{Prop}$ such that the set $\{(x, y) \in \beta \times \beta \mid p(x, y)\}$ is closed in $\beta \times \beta$, if $p(e(a_1), e(a_2))$ holds for all $a_1, a_2 \in \alpha$, then $p(b_1, b_2)$ holds for any $b_1, b_2 \in \beta$.

DenseRange.induction_on₃ theorem

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

Full source

@[elab_as_elim]
theorem DenseRange.induction_on₃ [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₃ :=
  isClosed_property3 he hp h _ _ _

Ternary Induction Principle for Dense Range Functions on Closed Predicates

Informal description

Let $\alpha$ and $\beta$ be topological spaces, and let $e \colon \alpha \to \beta$ be a function with dense range. For any ternary predicate $p \colon \beta \times \beta \times \beta \to \text{Prop}$ such that the set $\{(x, y, z) \in \beta^3 \mid p(x, y, z)\}$ is closed in $\beta^3$, if $p(e(a_1), e(a_2), e(a_3))$ holds for all $a_1, a_2, a_3 \in \alpha$, then $p(b_1, b_2, b_3)$ holds for any $b_1, b_2, b_3 \in \beta$.

DenseRange.equalizer theorem

(hfd : DenseRange f) {g h : β → γ} (hg : Continuous g) (hh : Continuous h) (H : g ∘ f = h ∘ f) : g = h

Full source

/-- Two continuous functions to a t2-space that agree on the dense range of a function are equal. -/
theorem DenseRange.equalizer (hfd : DenseRange f) {g h : β → γ} (hg : Continuous g)
    (hh : Continuous h) (H : g ∘ f = h ∘ f) : g = h :=
  funext fun y => hfd.induction_on y (isClosed_eq hg hh) <| congr_fun H

Uniqueness of Continuous Extensions on Dense Range in Hausdorff Spaces

Informal description

Let $f \colon \alpha \to \beta$ be a function with dense range between topological spaces, and let $g, h \colon \beta \to \gamma$ be continuous functions to a Hausdorff space $\gamma$. If $g \circ f = h \circ f$, then $g = h$.

Filter.HasBasis.hasBasis_of_isDenseInducing theorem

 [TopologicalSpace α] [TopologicalSpace β] [RegularSpace β] {ι : Type*} {s : ι → Set α} {p : ι → Prop} {x : α}
  (h : (𝓝 x).HasBasis p s) {f : α → β} (hf : IsDenseInducing f) : (𝓝 (f x)).HasBasis p fun i => closure <| f '' s i

Full source

theorem Filter.HasBasis.hasBasis_of_isDenseInducing [TopologicalSpace α] [TopologicalSpace β]
    [RegularSpace β] {ι : Type*} {s : ι → Set α} {p : ι → Prop} {x : α} (h : (𝓝 x).HasBasis p s)
    {f : α → β} (hf : IsDenseInducing f) : (𝓝 (f x)).HasBasis p fun i => closure <| f '' s i := by
  rw [Filter.hasBasis_iff] at h ⊢
  intro T
  refine ⟨fun hT => ?_, fun hT => ?_⟩
  · obtain ⟨T', hT₁, hT₂, hT₃⟩ := exists_mem_nhds_isClosed_subset hT
    have hT₄ : f ⁻¹' T'f ⁻¹' T' ∈ 𝓝 x := by
      rw [hf.isInducing.nhds_eq_comap x]
      exact ⟨T', hT₁, Subset.rfl⟩
    obtain ⟨i, hi, hi'⟩ := (h _).mp hT₄
    exact
      ⟨i, hi,
        (closure_mono (image_subset f hi')).trans
          (Subset.trans (closure_minimal (image_preimage_subset _ _) hT₂) hT₃)⟩
  · obtain ⟨i, hi, hi'⟩ := hT
    suffices closureclosure (f '' s i) ∈ 𝓝 (f x) by filter_upwards [this] using hi'
    replace h := (h (s i)).mpr ⟨i, hi, Subset.rfl⟩
    exact hf.closure_image_mem_nhds h

Neighborhood Basis Characterization for Dense Inducing Maps in Regular Spaces

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ regular, and let $f \colon X \to Y$ be a dense inducing map. Suppose that for a point $x \in X$, the neighborhood filter $\mathcal{N}_x$ has a basis $\{s_i \mid p i\}$ indexed by some type $\iota$. Then the neighborhood filter $\mathcal{N}_{f(x)}$ of $f(x)$ in $Y$ has a basis $\{\overline{f(s_i)} \mid p i\}$.