doc-next-gen

Mathlib.Topology.ContinuousMap.Basic

Module docstring

{"# Continuous bundled maps

In this file we define the type ContinuousMap of continuous bundled maps.

We use the DFunLike design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types. ","### Continuous maps "}

map_continuousAt theorem
(f : F) (a : α) : ContinuousAt f a
Full source 
theorem map_continuousAt (f : F) (a : α) : ContinuousAt f a :=
  (map_continuous f).continuousAt
Pointwise Continuity of Continuous Maps
Informal description
For any continuous map $f \colon \alpha \to \beta$ (where $F$ is a type of continuous maps between topological spaces $\alpha$ and $\beta$) and any point $a \in \alpha$, the function $f$ is continuous at $a$.
map_continuousWithinAt theorem
(f : F) (s : Set α) (a : α) : ContinuousWithinAt f s a
Full source 
theorem map_continuousWithinAt (f : F) (s : Set α) (a : α) : ContinuousWithinAt f s a :=
  (map_continuous f).continuousWithinAt
Continuity Within Subset for Continuous Maps
Informal description
For any continuous map $f \colon \alpha \to \beta$ (where $F$ is a type of continuous maps between topological spaces $\alpha$ and $\beta$), any subset $s \subseteq \alpha$, and any point $a \in \alpha$, the function $f$ is continuous within $s$ at $a$.
ContinuousMap.continuousAt theorem
(f : C(α, β)) (x : α) : ContinuousAt f x
Full source 
/-- Deprecated. Use `map_continuousAt` instead. -/
protected theorem continuousAt (f : C(α, β)) (x : α) : ContinuousAt f x :=
  map_continuousAt f x
Pointwise Continuity of Continuous Maps
Informal description
For any continuous map $f \colon \alpha \to \beta$ between topological spaces and any point $x \in \alpha$, the function $f$ is continuous at $x$.
ContinuousMap.map_specializes theorem
(f : C(α, β)) {x y : α} (h : x ⤳ y) : f x ⤳ f y
Full source 
theorem map_specializes (f : C(α, β)) {x y : α} (h : x ⤳ y) : f x ⤳ f y :=
  h.map f.2
Continuous Maps Preserve Specialization
Informal description
Let $f \colon \alpha \to \beta$ be a continuous map between topological spaces, and let $x, y \in \alpha$ be points such that $x$ specializes to $y$ (denoted $x \rightsquigarrow y$). Then $f(x)$ specializes to $f(y)$ in $\beta$, i.e., $f(x) \rightsquigarrow f(y)$.
ContinuousMap.equivFnOfDiscrete definition
[DiscreteTopology α] : C(α, β) ≃ (α → β)
Full source 
/--
The continuous functions from `α` to `β` are the same as the plain functions when `α` is discrete.
-/
@[simps]
def equivFnOfDiscrete [DiscreteTopology α] : C(α, β)C(α, β) ≃ (α → β) :=
  ⟨fun f => f,
    fun f => ⟨f, continuous_of_discreteTopology⟩,
    fun _ => by ext; rfl,
    fun _ => by ext; rfl⟩
Equivalence between continuous maps and functions on discrete spaces
Informal description
When the topological space $\alpha$ is discrete, there is a natural equivalence between the type of continuous maps from $\alpha$ to $\beta$ and the type of all functions from $\alpha$ to $\beta$. This equivalence is given by the identity map in both directions, since every function from a discrete space is continuous.
ContinuousMap.id definition
: C(α, α)
Full source 
/-- The identity as a continuous map. -/
protected def id : C(α, α) where
  toFun := id
Identity continuous map
Informal description
The identity continuous map from a topological space $\alpha$ to itself, defined by the identity function $\text{id} : \alpha \to \alpha$.
ContinuousMap.coe_id theorem
: ⇑(ContinuousMap.id α) = id
Full source 
@[simp, norm_cast]
theorem coe_id : ⇑(ContinuousMap.id α) = id :=
  rfl
Identity Continuous Map Coincides with Identity Function
Informal description
The underlying function of the identity continuous map on a topological space $\alpha$ is equal to the identity function $\text{id} : \alpha \to \alpha$.
ContinuousMap.const definition
(b : β) : C(α, β)
Full source 
/-- The constant map as a continuous map. -/
def const (b : β) : C(α, β) where
  toFun := fun _ : α => b
Constant continuous map
Informal description
The constant continuous map from a topological space $\alpha$ to a topological space $\beta$, defined by the function that maps every point in $\alpha$ to a fixed point $b \in \beta$.
ContinuousMap.coe_const theorem
(b : β) : ⇑(const α b) = Function.const α b
Full source 
@[simp]
theorem coe_const (b : β) : ⇑(const α b) = Function.const α b :=
  rfl
Constant Continuous Map Coincides with Constant Function
Informal description
For any fixed element $b$ in a topological space $\beta$, the underlying function of the constant continuous map from $\alpha$ to $\beta$ (which maps every point in $\alpha$ to $b$) is equal to the constant function $\alpha \to \beta$ that always returns $b$.
ContinuousMap.constPi definition
: C(β, α → β)
Full source 
/-- `Function.const α b` as a bundled continuous function of `b`. -/
@[simps -fullyApplied]
def constPi : C(β, α → β) where
  toFun b := Function.const α b
Constant function embedding into continuous function space
Informal description
The continuous map from a topological space $\beta$ to the space of continuous functions from $\alpha$ to $\beta$, where each point $b \in \beta$ is mapped to the constant function that sends every point in $\alpha$ to $b$.
ContinuousMap.instInhabited instance
[Inhabited β] : Inhabited C(α, β)
Full source 
instance [Inhabited β] : Inhabited C(α, β) :=
  ⟨const α default⟩
Inhabitedness of Continuous Function Space
Informal description
For any topological spaces $\alpha$ and $\beta$, if $\beta$ is inhabited (i.e., contains at least one element), then the space of continuous maps from $\alpha$ to $\beta$ is also inhabited.
ContinuousMap.id_apply theorem
(a : α) : ContinuousMap.id α a = a
Full source 
@[simp]
theorem id_apply (a : α) : ContinuousMap.id α a = a :=
  rfl
Identity Continuous Map Evaluation
Informal description
For any point $a$ in a topological space $\alpha$, the identity continuous map evaluated at $a$ equals $a$, i.e., $\text{id}(a) = a$.
ContinuousMap.const_apply theorem
(b : β) (a : α) : const α b a = b
Full source 
@[simp]
theorem const_apply (b : β) (a : α) : const α b a = b :=
  rfl
Evaluation of Constant Continuous Map: $(\text{const}_\alpha b)(a) = b$
Informal description
For any topological spaces $\alpha$ and $\beta$, a point $b \in \beta$, and a point $a \in \alpha$, the constant continuous map $\text{const}_\alpha b$ evaluated at $a$ equals $b$, i.e., $(\text{const}_\alpha b)(a) = b$.
ContinuousMap.comp definition
(f : C(β, γ)) (g : C(α, β)) : C(α, γ)
Full source 
/-- The composition of continuous maps, as a continuous map. -/
def comp (f : C(β, γ)) (g : C(α, β)) : C(α, γ) where
  toFun := f ∘ g
Composition of continuous maps
Informal description
The composition of continuous maps \( f \colon \beta \to \gamma \) and \( g \colon \alpha \to \beta \), yielding a continuous map \( \alpha \to \gamma \).
ContinuousMap.coe_comp theorem
(f : C(β, γ)) (g : C(α, β)) : ⇑(comp f g) = f ∘ g
Full source 
@[simp]
theorem coe_comp (f : C(β, γ)) (g : C(α, β)) : ⇑(comp f g) = f ∘ g :=
  rfl
Composition of Continuous Maps as Function Composition
Informal description
For any continuous maps $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ between topological spaces, the underlying function of their composition $f \circ g$ is equal to the composition of their underlying functions, i.e., $(f \circ g)(x) = f(g(x))$ for all $x \in \alpha$.
ContinuousMap.comp_apply theorem
(f : C(β, γ)) (g : C(α, β)) (a : α) : comp f g a = f (g a)
Full source 
@[simp]
theorem comp_apply (f : C(β, γ)) (g : C(α, β)) (a : α) : comp f g a = f (g a) :=
  rfl
Evaluation of Composition of Continuous Maps
Informal description
For any continuous maps \( f \colon \beta \to \gamma \) and \( g \colon \alpha \to \beta \), and any point \( a \in \alpha \), the composition \( f \circ g \) evaluated at \( a \) equals \( f \) evaluated at \( g(a) \), i.e., \((f \circ g)(a) = f(g(a))\).
ContinuousMap.comp_assoc theorem
(f : C(γ, δ)) (g : C(β, γ)) (h : C(α, β)) : (f.comp g).comp h = f.comp (g.comp h)
Full source 
@[simp]
theorem comp_assoc (f : C(γ, δ)) (g : C(β, γ)) (h : C(α, β)) :
    (f.comp g).comp h = f.comp (g.comp h) :=
  rfl
Associativity of Composition of Continuous Maps
Informal description
For any continuous maps $f \colon \gamma \to \delta$, $g \colon \beta \to \gamma$, and $h \colon \alpha \to \beta$, the composition of continuous maps is associative, i.e., $(f \circ g) \circ h = f \circ (g \circ h)$.
ContinuousMap.id_comp theorem
(f : C(α, β)) : (ContinuousMap.id _).comp f = f
Full source 
@[simp]
theorem id_comp (f : C(α, β)) : (ContinuousMap.id _).comp f = f :=
  ext fun _ => rfl
Left identity law for composition of continuous maps
Informal description
For any continuous map $f \colon \alpha \to \beta$ between topological spaces, the composition of the identity continuous map on $\beta$ with $f$ equals $f$, i.e., $\text{id}_\beta \circ f = f$.
ContinuousMap.comp_id theorem
(f : C(α, β)) : f.comp (ContinuousMap.id _) = f
Full source 
@[simp]
theorem comp_id (f : C(α, β)) : f.comp (ContinuousMap.id _) = f :=
  ext fun _ => rfl
Right Identity Law for Composition of Continuous Maps
Informal description
For any continuous map $f \colon \alpha \to \beta$ between topological spaces, the composition of $f$ with the identity continuous map on $\alpha$ equals $f$, i.e., $f \circ \text{id} = f$.
ContinuousMap.const_comp theorem
(c : γ) (f : C(α, β)) : (const β c).comp f = const α c
Full source 
@[simp]
theorem const_comp (c : γ) (f : C(α, β)) : (const β c).comp f = const α c :=
  ext fun _ => rfl
Composition of Constant Map with Continuous Map Yields Constant Map
Informal description
For any topological spaces $\alpha$, $\beta$, and $\gamma$, a constant continuous map $c \in \gamma$, and a continuous map $f \colon \alpha \to \beta$, the composition of the constant map with $f$ equals the constant map from $\alpha$ to $\gamma$ with value $c$. That is, $(c \circ f)(x) = c$ for all $x \in \alpha$.
ContinuousMap.comp_const theorem
(f : C(β, γ)) (b : β) : f.comp (const α b) = const α (f b)
Full source 
@[simp]
theorem comp_const (f : C(β, γ)) (b : β) : f.comp (const α b) = const α (f b) :=
  ext fun _ => rfl
Composition with Constant Map Yields Constant Map
Informal description
For any continuous map $f \colon \beta \to \gamma$ and any point $b \in \beta$, the composition of $f$ with the constant map $\text{const}_\alpha(b) \colon \alpha \to \beta$ (which maps every point in $\alpha$ to $b$) is equal to the constant map $\text{const}_\alpha(f(b)) \colon \alpha \to \gamma$ (which maps every point in $\alpha$ to $f(b)$).
ContinuousMap.cancel_right theorem
{f₁ f₂ : C(β, γ)} {g : C(α, β)} (hg : Surjective g) : f₁.comp g = f₂.comp g ↔ f₁ = f₂
Full source 
@[simp]
theorem cancel_right {f₁ f₂ : C(β, γ)} {g : C(α, β)} (hg : Surjective g) :
    f₁.comp g = f₂.comp g ↔ f₁ = f₂ :=
  ⟨fun h => ext <| hg.forall.2 <| DFunLike.ext_iff.1 h, congr_arg (ContinuousMap.comp · g)⟩
Right Cancellation Property for Composition of Continuous Maps under Surjectivity
Informal description
Let $X$, $Y$, and $Z$ be topological spaces, and let $f_1, f_2 \colon Y \to Z$ and $g \colon X \to Y$ be continuous maps. If $g$ is surjective, then the compositions $f_1 \circ g$ and $f_2 \circ g$ are equal if and only if $f_1 = f_2$.
ContinuousMap.cancel_left theorem
{f : C(β, γ)} {g₁ g₂ : C(α, β)} (hf : Injective f) : f.comp g₁ = f.comp g₂ ↔ g₁ = g₂
Full source 
@[simp]
theorem cancel_left {f : C(β, γ)} {g₁ g₂ : C(α, β)} (hf : Injective f) :
    f.comp g₁ = f.comp g₂ ↔ g₁ = g₂ :=
  ⟨fun h => ext fun a => hf <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩
Left Cancellation Property for Composition of Continuous Maps under Injectivity
Informal description
Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon Y \to Z$ and $g_1, g_2 \colon X \to Y$ be continuous maps. If $f$ is injective, then the compositions $f \circ g_1$ and $f \circ g_2$ are equal if and only if $g_1 = g_2$.
ContinuousMap.instNontrivialOfNonempty instance
[Nonempty α] [Nontrivial β] : Nontrivial C(α, β)
Full source 
instance [Nonempty α] [Nontrivial β] : Nontrivial C(α, β) :=
  ⟨let ⟨b₁, b₂, hb⟩ := exists_pair_ne β
  ⟨const _ b₁, const _ b₂, fun h => hb <| DFunLike.congr_fun h <| Classical.arbitrary α⟩⟩
Nontriviality of Continuous Function Space for Nonempty Domain and Nontrivial Codomain
Informal description
For any nonempty topological space $\alpha$ and nontrivial topological space $\beta$, the space of continuous maps $C(\alpha, \beta)$ is nontrivial.
ContinuousMap.fst definition
: C(α × β, α)
Full source 
/-- `Prod.fst : (x, y) ↦ x` as a bundled continuous map. -/
@[simps -fullyApplied]
def fst : C(α × β, α) where
  toFun := Prod.fst
First projection continuous map
Informal description
The continuous map $\pi_1 \colon X \times Y \to X$ that projects a pair $(x, y)$ to its first component $x$, where $X$ and $Y$ are topological spaces and $X \times Y$ is equipped with the product topology.
ContinuousMap.snd definition
: C(α × β, β)
Full source 
/-- `Prod.snd : (x, y) ↦ y` as a bundled continuous map. -/
@[simps -fullyApplied]
def snd : C(α × β, β) where
  toFun := Prod.snd
Second projection as a continuous map
Informal description
The second projection map $(x, y) \mapsto y$ from the product space $\alpha \times \beta$ to $\beta$, viewed as a continuous map between topological spaces.
ContinuousMap.prodMk definition
(f : C(α, β₁)) (g : C(α, β₂)) : C(α, β₁ × β₂)
Full source 
/-- Given two continuous maps `f` and `g`, this is the continuous map `x ↦ (f x, g x)`. -/
def prodMk (f : C(α, β₁)) (g : C(α, β₂)) : C(α, β₁ × β₂) where
  toFun x := (f x, g x)
Continuous map to product space
Informal description
Given two continuous maps \( f \colon X \to Y_1 \) and \( g \colon X \to Y_2 \) between topological spaces, this defines the continuous map \( x \mapsto (f(x), g(x)) \) from \( X \) to the product space \( Y_1 \times Y_2 \).
ContinuousMap.prodMap definition
(f : C(α₁, α₂)) (g : C(β₁, β₂)) : C(α₁ × β₁, α₂ × β₂)
Full source 
/-- Given two continuous maps `f` and `g`, this is the continuous map `(x, y) ↦ (f x, g y)`. -/
@[simps]
def prodMap (f : C(α₁, α₂)) (g : C(β₁, β₂)) : C(α₁ × β₁, α₂ × β₂) where
  toFun := Prod.map f g
Product of continuous maps
Informal description
Given two continuous maps \( f \colon \alpha_1 \to \alpha_2 \) and \( g \colon \beta_1 \to \beta_2 \), this is the continuous map \( (x, y) \mapsto (f x, g y) \) from \( \alpha_1 \times \beta_1 \) to \( \alpha_2 \times \beta_2 \).
ContinuousMap.prod_eval theorem
(f : C(α, β₁)) (g : C(α, β₂)) (a : α) : (prodMk f g) a = (f a, g a)
Full source 
@[simp]
theorem prod_eval (f : C(α, β₁)) (g : C(α, β₂)) (a : α) : (prodMk f g) a = (f a, g a) :=
  rfl
Evaluation of Product Continuous Map at Point
Informal description
For any continuous maps $f \colon X \to Y_1$ and $g \colon X \to Y_2$ between topological spaces, and for any point $a \in X$, the evaluation of the product map $\mathrm{prodMk}\,f\,g$ at $a$ equals the pair $(f(a), g(a))$.
ContinuousMap.prodSwap definition
: C(α × β, β × α)
Full source 
/-- `Prod.swap` bundled as a `ContinuousMap`. -/
@[simps!]
def prodSwap : C(α × β, β × α) := .prodMk .snd .fst
Continuous swap map on product spaces
Informal description
The continuous map that swaps the components of a pair in the product space \( \alpha \times \beta \), i.e., the map \( (x, y) \mapsto (y, x) \).
ContinuousMap.sigmaMk definition
(i : I) : C(X i, Σ i, X i)
Full source 
/-- `Sigma.mk i` as a bundled continuous map. -/
@[simps apply]
def sigmaMk (i : I) : C(X i, Σ i, X i) where
  toFun := Sigma.mk i
Continuous inclusion into disjoint union space
Informal description
For each index $i$ in the index set $I$, the function `ContinuousMap.sigmaMk` is the continuous inclusion map from the topological space $X_i$ into the disjoint union $\Sigma_{i} X_i$ (equipped with the disjoint union topology), defined by sending each $x \in X_i$ to the pair $(i, x)$.
ContinuousMap.sigma definition
(f : ∀ i, C(X i, A)) : C((Σ i, X i), A)
Full source 
/--
To give a continuous map out of a disjoint union, it suffices to give a continuous map out of
each term. This is `Sigma.uncurry` for continuous maps.
-/
@[simps]
def sigma (f : ∀ i, C(X i, A)) : C((Σ i, X i), A) where
  toFun ig := f ig.fst ig.snd
Continuous map from disjoint union induced by family of continuous maps
Informal description
Given a family of continuous maps \( f_i : X_i \to A \) for each \( i \) in some index set, the function `ContinuousMap.sigma` constructs a continuous map from the disjoint union \( \Sigma_i X_i \) to \( A \) by applying the appropriate \( f_i \) to each point in \( X_i \). Specifically, for a point \( (i, x) \) in \( \Sigma_i X_i \), the map evaluates to \( f_i(x) \).
ContinuousMap.sigmaEquiv definition
: (∀ i, C(X i, A)) ≃ C((Σ i, X i), A)
Full source 
/--
Giving a continuous map out of a disjoint union is the same as giving a continuous map out of
each term. This is a version of `Equiv.piCurry` for continuous maps.
-/
@[simps]
def sigmaEquiv : (∀ i, C(X i, A)) ≃ C((Σ i, X i), A) where
  toFun := sigma
  invFun f i := f.comp (sigmaMk i)
  left_inv := by intro; ext; simp
  right_inv := by intro; ext; simp
Equivalence between families of continuous maps and continuous maps on disjoint unions
Informal description
The equivalence between the type of families of continuous maps \( (f_i \colon X_i \to A)_{i \in I} \) and the type of continuous maps from the disjoint union \( \Sigma_i X_i \) to \( A \). Specifically: 1. The forward direction (`toFun`) takes a family \( (f_i)_{i \in I} \) and constructs the continuous map \( \Sigma_i X_i \to A \) by applying \( f_i \) to each point in \( X_i \). 2. The inverse direction (`invFun`) takes a continuous map \( f \colon \Sigma_i X_i \to A \) and recovers the family \( (f \circ \sigma_i)_{i \in I} \), where \( \sigma_i \colon X_i \to \Sigma_i X_i \) is the inclusion map. 3. The equivalence is bijective, with the left inverse (`left_inv`) and right inverse (`right_inv`) properties ensuring that applying `toFun` and `invFun` in either order returns the original object.
ContinuousMap.pi definition
(f : ∀ i, C(A, X i)) : C(A, ∀ i, X i)
Full source 
/-- Abbreviation for product of continuous maps, which is continuous -/
def pi (f : ∀ i, C(A, X i)) : C(A, ∀ i, X i) where
  toFun (a : A) (i : I) := f i a
Continuous map into product space induced by family of continuous maps
Informal description
Given a family of continuous maps \( f_i : A \to X_i \) for each \( i \) in some index set \( I \), the function `ContinuousMap.pi` constructs a continuous map from \( A \) to the product space \( \prod_{i \in I} X_i \) by applying each \( f_i \) to the input point. Specifically, for a point \( a \in A \), the map evaluates to \( (f_i(a))_{i \in I} \).
ContinuousMap.pi_eval theorem
(f : ∀ i, C(A, X i)) (a : A) : (pi f) a = fun i : I => (f i) a
Full source 
@[simp]
theorem pi_eval (f : ∀ i, C(A, X i)) (a : A) : (pi f) a = fun i : I => (f i) a :=
  rfl
Evaluation of Product of Continuous Maps
Informal description
For any family of continuous maps \( f_i : A \to X_i \) indexed by \( i \in I \) and any point \( a \in A \), the evaluation of the product map \( \pi f \) at \( a \) is equal to the function \( \lambda i, f_i(a) \), i.e., \( (\pi f)(a) = (f_i(a))_{i \in I} \).
ContinuousMap.eval definition
(i : I) : C(∀ j, X j, X i)
Full source 
/-- Evaluation at point as a bundled continuous map. -/
@[simps -fullyApplied]
def eval (i : I) : C(∀ j, X j, X i) where
  toFun := Function.eval i
Continuous evaluation map at index \( i \)
Informal description
For each index \( i \) in the index set \( I \), the evaluation map \( \text{eval}_i \colon \prod_{j \in I} X_j \to X_i \) is a continuous function, where \( \prod_{j \in I} X_j \) is equipped with the product topology.
ContinuousMap.piEquiv definition
: (∀ i, C(A, X i)) ≃ C(A, ∀ i, X i)
Full source 
/--
Giving a continuous map out of a disjoint union is the same as giving a continuous map out of
each term
-/
@[simps]
def piEquiv : (∀ i, C(A, X i)) ≃ C(A, ∀ i, X i) where
  toFun := pi
  invFun f i := (eval i).comp f
  left_inv := by intro; ext; simp [pi]
  right_inv := by intro; ext; simp [pi]
Equivalence between families of continuous maps and product-space-valued continuous maps
Informal description
The equivalence between the type of families of continuous maps $(f_i \colon A \to X_i)_{i \in I}$ and the type of continuous maps from $A$ to the product space $\prod_{i \in I} X_i$. The forward direction combines a family of continuous maps into a single continuous map to the product space (via `ContinuousMap.pi`), while the inverse direction decomposes a product-space-valued continuous map into its component functions (via composition with evaluation maps `eval i`).
ContinuousMap.piMap definition
(f : ∀ i, C(X i, Y i)) : C((i : I) → X i, (i : I) → Y i)
Full source 
/-- Combine a collection of bundled continuous maps `C(X i, Y i)` into a bundled continuous map
`C(∀ i, X i, ∀ i, Y i)`. -/
@[simps!]
def piMap (f : ∀ i, C(X i, Y i)) : C((i : I) → X i, (i : I) → Y i) :=
  .pi fun i ↦ (f i).comp (eval i)
Continuous map between product spaces induced by a family of continuous maps
Informal description
Given a family of continuous maps \( f_i \colon X_i \to Y_i \) for each \( i \) in an index set \( I \), the function `ContinuousMap.piMap` constructs a continuous map from the product space \( \prod_{i \in I} X_i \) to the product space \( \prod_{i \in I} Y_i \) by applying each \( f_i \) to the corresponding component of the input. Specifically, for a point \( (x_i)_{i \in I} \in \prod_{i \in I} X_i \), the map evaluates to \( (f_i(x_i))_{i \in I} \).
ContinuousMap.precomp definition
{ι : Type*} (φ : ι → I) : C((i : I) → X i, (i : ι) → X (φ i))
Full source 
/-- "Precomposition" as a continuous map between dependent types. -/
def precomp {ι : Type*} (φ : ι → I) : C((i : I) → X i, (i : ι) → X (φ i)) :=
  ⟨_, Pi.continuous_precomp' φ⟩
Precomposition as a continuous map between product spaces
Informal description
Given a function $\varphi \colon \iota \to I$ between index sets, the precomposition map $f \mapsto (f \circ \varphi) \colon \prod_{i \in I} X_i \to \prod_{j \in \iota} X_{\varphi(j)}$ is a continuous map between the product spaces equipped with their product topologies.
ContinuousMap.restrict definition
(f : C(α, β)) : C(s, β)
Full source 
/-- The restriction of a continuous function `α → β` to a subset `s` of `α`. -/
def restrict (f : C(α, β)) : C(s, β) where
  toFun := f ∘ ((↑) : s → α)
Restriction of a continuous map to a subset
Informal description
Given a continuous map \( f \colon C(\alpha, \beta) \) between topological spaces \( \alpha \) and \( \beta \), and a subset \( s \subseteq \alpha \), the restriction of \( f \) to \( s \) is the continuous map \( f|_s \colon C(s, \beta) \) defined by \( f|_s(x) = f(x) \) for all \( x \in s \).
ContinuousMap.coe_restrict theorem
(f : C(α, β)) : ⇑(f.restrict s) = f ∘ ((↑) : s → α)
Full source 
@[simp]
theorem coe_restrict (f : C(α, β)) : ⇑(f.restrict s) = f ∘ ((↑) : s → α) :=
  rfl
Restriction of a Continuous Map as Composition with Inclusion
Informal description
For any continuous map $f \colon C(\alpha, \beta)$ between topological spaces $\alpha$ and $\beta$, and any subset $s \subseteq \alpha$, the underlying function of the restriction $f|_s$ is equal to the composition of $f$ with the inclusion map $s \hookrightarrow \alpha$. That is, $f|_s = f \circ \iota$, where $\iota \colon s \to \alpha$ is the inclusion map.
ContinuousMap.restrict_apply theorem
(f : C(α, β)) (s : Set α) (x : s) : f.restrict s x = f x
Full source 
@[simp]
theorem restrict_apply (f : C(α, β)) (s : Set α) (x : s) : f.restrict s x = f x :=
  rfl
Restriction of Continuous Map Preserves Evaluation
Informal description
Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a continuous map, and $s \subseteq X$ a subset. For any $x \in s$, the restriction $f|_s$ evaluated at $x$ equals $f$ evaluated at $x$, i.e., $f|_s(x) = f(x)$.
ContinuousMap.restrict_apply_mk theorem
(f : C(α, β)) (s : Set α) (x : α) (hx : x ∈ s) : f.restrict s ⟨x, hx⟩ = f x
Full source 
@[simp]
theorem restrict_apply_mk (f : C(α, β)) (s : Set α) (x : α) (hx : x ∈ s) :
    f.restrict s ⟨x, hx⟩ = f x :=
  rfl
Restriction of Continuous Map Evaluates to Original Function
Informal description
Let $f \colon C(\alpha, \beta)$ be a continuous map between topological spaces $\alpha$ and $\beta$, and let $s \subseteq \alpha$ be a subset. For any $x \in \alpha$ with $x \in s$, the restriction $f|_s$ evaluated at the point $\langle x, hx \rangle$ (where $hx$ is the proof that $x \in s$) equals $f(x)$. In other words, $f|_s(\langle x, hx \rangle) = f(x)$.
ContinuousMap.injective_restrict theorem
[T2Space β] {s : Set α} (hs : Dense s) : Injective (restrict s : C(α, β) → C(s, β))
Full source 
theorem injective_restrict [T2Space β] {s : Set α} (hs : Dense s) :
    Injective (restrict s : C(α, β) → C(s, β)) := fun f g h ↦
  DFunLike.ext' <| (map_continuous f).ext_on hs (map_continuous g) <|
    Set.restrict_eq_restrict_iff.1 <| congr_arg DFunLike.coe h
Injectivity of Continuous Function Restriction to Dense Subset in Hausdorff Spaces
Informal description
Let $X$ and $Y$ be topological spaces with $Y$ Hausdorff, and let $s \subseteq X$ be a dense subset. Then the restriction map $\text{restrict}_s : C(X, Y) \to C(s, Y)$, which sends a continuous function $f$ to its restriction $f|_s$, is injective.
ContinuousMap.restrictPreimage definition
(f : C(α, β)) (s : Set β) : C(f ⁻¹' s, s)
Full source 
/-- The restriction of a continuous map to the preimage of a set. -/
@[simps]
def restrictPreimage (f : C(α, β)) (s : Set β) : C(f ⁻¹' s, s) :=
  ⟨s.restrictPreimage f, continuous_iff_continuousAt.mpr fun _ ↦
    (map_continuousAt f _).restrictPreimage⟩
Restriction of a continuous map to its preimage
Informal description
Given a continuous map \( f : C(\alpha, \beta) \) between topological spaces and a subset \( s \subseteq \beta \), the function `ContinuousMap.restrictPreimage` restricts \( f \) to a continuous map from the preimage \( f^{-1}(s) \) to \( s \).
ContinuousMap.liftCover definition
: C(α, β)
Full source 
/-- A family `φ i` of continuous maps `C(S i, β)`, where the domains `S i` contain a neighbourhood
of each point in `α` and the functions `φ i` agree pairwise on intersections, can be glued to
construct a continuous map in `C(α, β)`. -/
noncomputable def liftCover : C(α, β) :=
  haveI H : ⋃ i, S i = Set.univ :=
    Set.iUnion_eq_univ_iff.2 fun x ↦ (hS x).imp fun _ ↦ mem_of_mem_nhds
  mk (Set.liftCover S (fun i ↦ φ i) hφ H) <| continuous_of_cover_nhds hS fun i ↦ by
    rw [continuousOn_iff_continuous_restrict]
    simpa +unfoldPartialApp only [Set.restrict, Set.liftCover_coe]
      using map_continuous (φ i)
Gluing of continuous maps on a cover of sets
Informal description
Given an indexed family of sets \( S_i \subseteq \alpha \) covering the entire space \(\alpha\) (i.e., \(\bigcup_i S_i = \alpha\)), and a family of continuous maps \( \varphi_i : C(S_i, \beta) \) that agree on pairwise intersections (i.e., for any \( i, j \) and \( x \in S_i \cap S_j \), \( \varphi_i(x) = \varphi_j(x) \)), the function `ContinuousMap.liftCover` constructs a continuous map from \(\alpha\) to \(\beta\) by gluing the maps \( \varphi_i \) together. Specifically, for any \( x \in \alpha \), it selects an index \( i \) such that \( x \in S_i \) and returns \( \varphi_i(x) \).
ContinuousMap.liftCover_coe theorem
{i : ι} (x : S i) : liftCover S φ hφ hS x = φ i x
Full source 
@[simp]
theorem liftCover_coe {i : ι} (x : S i) : liftCover S φ hφ hS x = φ i x := by
  rw [liftCover, coe_mk, Set.liftCover_coe _]
Lifted Continuous Map Agrees with Component Maps on Their Domains
Informal description
For any index $i$ and any element $x$ in the subset $S_i \subseteq \alpha$, the value of the lifted continuous map $\mathrm{liftCover}(S, \varphi, h\varphi, hS)$ at $x$ equals the value of the continuous map $\varphi_i$ at $x$, i.e., \[ \mathrm{liftCover}(S, \varphi, h\varphi, hS)(x) = \varphi_i(x). \] Here, $S : \iota \to \text{Set } \alpha$ is a family of subsets covering $\alpha$ (i.e., $\bigcup_i S_i = \alpha$), $\varphi_i : C(S_i, \beta)$ are continuous maps that agree on pairwise intersections, $h\varphi$ is the proof of pairwise agreement, and $hS$ is the proof that the union covers $\alpha$.
ContinuousMap.liftCover_restrict theorem
{i : ι} : (liftCover S φ hφ hS).restrict (S i) = φ i
Full source 
@[simp]
theorem liftCover_restrict {i : ι} : (liftCover S φ hφ hS).restrict (S i) = φ i := by
  ext
  simp only [coe_restrict, Function.comp_apply, liftCover_coe]
Restriction of Lifted Continuous Map Equals Component Map on Its Domain
Informal description
For any index $i$, the restriction of the lifted continuous map $\mathrm{liftCover}(S, \varphi, h\varphi, hS)$ to the subset $S_i \subseteq \alpha$ equals the continuous map $\varphi_i \colon C(S_i, \beta)$. That is, \[ \left(\mathrm{liftCover}(S, \varphi, h\varphi, hS)\right)\big|_{S_i} = \varphi_i, \] where $S \colon \iota \to \text{Set } \alpha$ is a family of subsets covering $\alpha$, $\varphi_i \colon C(S_i, \beta)$ are continuous maps agreeing on pairwise intersections, $h\varphi$ is the proof of agreement, and $hS$ is the proof that $\bigcup_i S_i = \alpha$.
ContinuousMap.liftCover' definition
: C(α, β)
Full source 
/-- A family `F s` of continuous maps `C(s, β)`, where (1) the domains `s` are taken from a set `A`
of sets in `α` which contain a neighbourhood of each point in `α` and (2) the functions `F s` agree
pairwise on intersections, can be glued to construct a continuous map in `C(α, β)`. -/
noncomputable def liftCover' : C(α, β) :=
  let F : ∀ i : A, C(i, β) := fun i => F i i.prop
  liftCover ((↑) : A → Set α) F (fun i j => hF i i.prop j j.prop)
    fun x => let ⟨s, hs, hsx⟩ := hA x; ⟨⟨s, hs⟩, hsx⟩
Gluing of continuous maps on a cover of neighborhoods
Informal description
Given a family of continuous maps \( F_s : C(s, \beta) \) indexed by sets \( s \) in a collection \( A \) of subsets of \( \alpha \), where: 1. Each \( s \in A \) contains a neighborhood of every point in \( \alpha \), 2. The maps \( F_s \) agree on pairwise intersections (i.e., \( F_s(x) = F_{s'}(x) \) for all \( x \in s \cap s' \)), the function `ContinuousMap.liftCover'` constructs a continuous map from \( \alpha \) to \( \beta \) by gluing the maps \( F_s \) together. Specifically, for any \( x \in \alpha \), it selects a set \( s \in A \) containing \( x \) and returns \( F_s(x) \).
ContinuousMap.liftCover_coe' theorem
{s : Set α} {hs : s ∈ A} (x : s) : liftCover' A F hF hA x = F s hs x
Full source 
@[simp]
theorem liftCover_coe' {s : Set α} {hs : s ∈ A} (x : s) : liftCover' A F hF hA x = F s hs x :=
  let x' : ((↑) : A → Set α) ⟨s, hs⟩ := x
  by delta liftCover'; exact ContinuousMap.liftCover_coe x'
Lifted Continuous Map Agrees with Component Maps on Their Domains
Informal description
For any set $s$ in a collection $A$ of subsets of a topological space $\alpha$, and for any point $x$ in $s$, the value of the lifted continuous map $\mathrm{liftCover'}(A, F, hF, hA)$ at $x$ equals the value of the continuous map $F_s$ at $x$, i.e., \[ \mathrm{liftCover'}(A, F, hF, hA)(x) = F_s(x). \] Here, $F_s : C(s, \beta)$ is a continuous map defined on $s$, $hF$ is the proof that the maps $F_s$ agree on pairwise intersections, and $hA$ is the proof that every point in $\alpha$ has a neighborhood in some $s \in A$.
ContinuousMap.liftCover_restrict' theorem
{s : Set α} {hs : s ∈ A} : (liftCover' A F hF hA).restrict s = F s hs
Full source 
@[simp]
theorem liftCover_restrict' {s : Set α} {hs : s ∈ A} :
    (liftCover' A F hF hA).restrict s = F s hs := ext <| liftCover_coe' (hF := hF) (hA := hA)
Restriction of Lifted Continuous Map Equals Component Map
Informal description
For any set $s$ in a collection $A$ of subsets of a topological space $\alpha$, the restriction of the lifted continuous map $\mathrm{liftCover'}(A, F, hF, hA)$ to $s$ equals the continuous map $F_s$ defined on $s$. That is, \[ \left(\mathrm{liftCover'}(A, F, hF, hA)\right)|_s = F_s. \] Here, $F_s : C(s, \beta)$ is a continuous map defined on $s$, $hF$ is the proof that the maps $F_s$ agree on pairwise intersections, and $hA$ is the proof that every point in $\alpha$ has a neighborhood in some $s \in A$.
ContinuousMap.inclusion definition
{s t : Set α} (h : s ⊆ t) : C(s, t)
Full source 
/-- `Set.inclusion` as a bundled continuous map. -/
def inclusion {s t : Set α} (h : s ⊆ t) : C(s, t) where
  toFun := Set.inclusion h
  continuous_toFun := continuous_inclusion h
Continuous inclusion map between subsets
Informal description
Given a topological space $\alpha$ and subsets $s, t \subseteq \alpha$ such that $s \subseteq t$, the bundled continuous map $\text{inclusion}(h) : C(s, t)$ is the canonical inclusion function from $s$ to $t$ equipped with the subspace topology, where the continuity is guaranteed by the subspace topology construction.
Function.RightInverse.homeomorph definition
{f' : C(Y, X)} (hf : Function.RightInverse f' f) : Quotient (Setoid.ker f) ≃ₜ Y
Full source 
/-- `Setoid.quotientKerEquivOfRightInverse` as a homeomorphism. -/
@[simps!]
def Function.RightInverse.homeomorph {f' : C(Y, X)} (hf : Function.RightInverse f' f) :
    QuotientQuotient (Setoid.ker f) ≃ₜ Y where
  toEquiv := Setoid.quotientKerEquivOfRightInverse _ _ hf
  continuous_toFun := isQuotientMap_quot_mk.continuous_iff.mpr (map_continuous f)
  continuous_invFun := continuous_quotient_mk'.comp (map_continuous f')
Homeomorphism from quotient by kernel to codomain via right inverse
Informal description
Given a continuous map \( f : X \to Y \) between topological spaces and a continuous right inverse \( f' : Y \to X \) (i.e., \( f \circ f' = \text{id}_Y \)), the quotient space \( X / \ker f \) is homeomorphic to \( Y \). Here, \( \ker f \) is the equivalence relation on \( X \) defined by \( x \sim y \) if and only if \( f(x) = f(y) \). The homeomorphism is induced by the equivalence \( X / \ker f \simeq Y \) and the continuity of \( f \) and \( f' \).
Topology.IsQuotientMap.homeomorph definition
(hf : IsQuotientMap f) : Quotient (Setoid.ker f) ≃ₜ Y
Full source 
/--
The homeomorphism from the quotient of a quotient map to its codomain. This is
`Setoid.quotientKerEquivOfSurjective` as a homeomorphism.
-/
@[simps!]
noncomputable def homeomorph (hf : IsQuotientMap f) : QuotientQuotient (Setoid.ker f) ≃ₜ Y where
  toEquiv := Setoid.quotientKerEquivOfSurjective _ hf.surjective
  continuous_toFun := isQuotientMap_quot_mk.continuous_iff.mpr hf.continuous
  continuous_invFun := by
    rw [hf.continuous_iff]
    convert continuous_quotient_mk'
    ext
    simp only [Equiv.invFun_as_coe, Function.comp_apply,
      (Setoid.quotientKerEquivOfSurjective f hf.surjective).symm_apply_eq]
    rfl
Homeomorphism from quotient by kernel to codomain for a quotient map
Informal description
Given a quotient map \( f : X \to Y \) between topological spaces, the quotient space \( X / \ker f \) is homeomorphic to \( Y \). Here, \( \ker f \) is the equivalence relation on \( X \) defined by \( x \sim y \) if and only if \( f(x) = f(y) \). The homeomorphism is induced by the canonical bijection between \( X / \ker f \) and \( Y \), and the continuity of \( f \) ensures that this bijection is a homeomorphism.
Topology.IsQuotientMap.lift definition
: C(Y, Z)
Full source 
/-- Descend a continuous map, which is constant on the fibres, along a quotient map. -/
@[simps]
noncomputable def lift : C(Y, Z) where
  toFun := ((fun i ↦ Quotient.liftOn' i g (fun _ _ (hab : f _ = f _) ↦ h hab)) :
    Quotient (Setoid.ker f) → Z) ∘ hf.homeomorph.symm
  continuous_toFun := Continuous.comp (continuous_quot_lift _ g.2) (Homeomorph.continuous _)
Lifting a continuous map along a quotient map
Informal description
Given a quotient map \( f : X \to Y \) between topological spaces and a continuous map \( g : X \to Z \) that is constant on the fibers of \( f \) (i.e., \( g(x) = g(y) \) whenever \( f(x) = f(y) \)), the function `Topology.IsQuotientMap.lift` constructs a continuous map \( Y \to Z \) that descends \( g \) along \( f \). Specifically, this map is obtained by first lifting \( g \) to the quotient space \( X / \ker f \) and then composing with the homeomorphism \( Y \simeq X / \ker f \) induced by \( f \).
Topology.IsQuotientMap.lift_comp theorem
: (hf.lift g h).comp f = g
Full source 
/--
The obvious triangle induced by `IsQuotientMap.lift` commutes:
```
     g
  X --→ Z
  |   ↗
f |  / hf.lift g h
  v /
  Y
```
-/
@[simp]
theorem lift_comp : (hf.lift g h).comp f = g := by
  ext
  simpa using h (Function.rightInverse_surjInv _ _)
Commutativity of the lifting diagram for quotient maps
Informal description
Let $f \colon X \to Y$ be a quotient map between topological spaces, and let $g \colon X \to Z$ be a continuous map that is constant on the fibers of $f$ (i.e., $g(x) = g(y)$ whenever $f(x) = f(y)$). Then the lifted continuous map $h = \text{lift}(f, g) \colon Y \to Z$ satisfies $h \circ f = g$.
Topology.IsQuotientMap.liftEquiv definition
: { g : C(X, Z) // Function.FactorsThrough g f } ≃ C(Y, Z)
Full source 
/-- `IsQuotientMap.lift` as an equivalence. -/
@[simps]
noncomputable def liftEquiv : { g : C(X, Z) // Function.FactorsThrough g f}{ g : C(X, Z) // Function.FactorsThrough g f} ≃ C(Y, Z) where
  toFun g := hf.lift g g.prop
  invFun g := ⟨g.comp f, fun _ _ h ↦ by simp only [ContinuousMap.comp_apply]; rw [h]⟩
  left_inv := by intro; simp
  right_inv := by
    intro g
    ext a
    simpa using congrArg g (Function.rightInverse_surjInv hf.surjective a)
Equivalence between continuous maps factoring through a quotient map and continuous maps on the quotient space
Informal description
Given a quotient map \( f \colon X \to Y \) between topological spaces, the equivalence `Topology.IsQuotientMap.liftEquiv` establishes a bijection between the set of continuous maps \( g \colon X \to Z \) that factor through \( f \) (i.e., \( g \) is constant on the fibers of \( f \)) and the set of continuous maps \( Y \to Z \). Specifically: - The forward direction takes a continuous map \( g \colon X \to Z \) that factors through \( f \) and constructs the unique continuous map \( Y \to Z \) descending \( g \). - The backward direction takes a continuous map \( Y \to Z \) and precomposes it with \( f \). This equivalence is natural in the sense that the composition of the lifted map with \( f \) recovers the original map \( g \), and conversely, any continuous map \( Y \to Z \) is uniquely determined by its precomposition with \( f \).
Homeomorph.instContinuousMapClass instance
: ContinuousMapClass (α ≃ₜ β) α β
Full source 
instance instContinuousMapClass : ContinuousMapClass (α ≃ₜ β) α β where
  map_continuous f := f.continuous_toFun
Homeomorphisms are Continuous Maps
Informal description
Every homeomorphism between topological spaces $\alpha$ and $\beta$ is a continuous map.
Homeomorph.coe_refl theorem
: (Homeomorph.refl α : C(α, α)) = ContinuousMap.id α
Full source 
@[simp]
theorem coe_refl : (Homeomorph.refl α : C(α, α)) = ContinuousMap.id α :=
  rfl
Identity Homeomorphism as Identity Continuous Map
Informal description
The bundled continuous map corresponding to the identity homeomorphism on a topological space $\alpha$ is equal to the identity continuous map on $\alpha$.
Homeomorph.coe_trans theorem
: (f.trans g : C(α, γ)) = (g : C(β, γ)).comp f
Full source 
@[simp]
theorem coe_trans : (f.trans g : C(α, γ)) = (g : C(β, γ)).comp f :=
  rfl
Composition of Homeomorphisms as Continuous Maps
Informal description
For any homeomorphisms $f \colon \alpha \simeq \beta$ and $g \colon \beta \simeq \gamma$ between topological spaces, the bundled continuous map associated with their composition $f \circ g$ is equal to the composition of the bundled continuous maps associated with $g$ and $f$, i.e., $(f \circ g) = g \circ f$ as continuous maps.
Homeomorph.symm_comp_toContinuousMap theorem
: (f.symm : C(β, α)).comp (f : C(α, β)) = ContinuousMap.id α
Full source 
/-- Left inverse to a continuous map from a homeomorphism, mirroring `Equiv.symm_comp_self`. -/
@[simp]
theorem symm_comp_toContinuousMap :
    (f.symm : C(β, α)).comp (f : C(α, β)) = ContinuousMap.id α := by
  rw [← coe_trans, self_trans_symm, coe_refl]
Composition of Homeomorphism with its Inverse Yields Identity on Domain
Informal description
For any homeomorphism $f \colon \alpha \to \beta$ between topological spaces $\alpha$ and $\beta$, the composition of the continuous map associated with the inverse homeomorphism $f^{-1} \colon \beta \to \alpha$ and the continuous map associated with $f$ is equal to the identity continuous map on $\alpha$, i.e., $f^{-1} \circ f = \text{id}_\alpha$.
Homeomorph.toContinuousMap_comp_symm theorem
: (f : C(α, β)).comp (f.symm : C(β, α)) = ContinuousMap.id β
Full source 
/-- Right inverse to a continuous map from a homeomorphism, mirroring `Equiv.self_comp_symm`. -/
@[simp]
theorem toContinuousMap_comp_symm :
    (f : C(α, β)).comp (f.symm : C(β, α)) = ContinuousMap.id β := by
  rw [← coe_trans, symm_trans_self, coe_refl]
Composition of Homeomorphism with its Inverse Yields Identity
Informal description
For any homeomorphism $f \colon \alpha \simeq \beta$ between topological spaces $\alpha$ and $\beta$, the composition of the continuous map $f \colon C(\alpha, \beta)$ with its inverse $f^{-1} \colon C(\beta, \alpha)$ yields the identity continuous map on $\beta$, i.e., $f \circ f^{-1} = \text{id}_\beta$.