ContinuousMap.ext
theorem ContinuousMap.ext :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : C(α, β)},
(∀ (a : α), f a = g a) → f = g
This theorem states that for any two continuous maps `f` and `g` from a topological space `α` to another topological space `β`, if for every element `a` in `α` the value of `f` at `a` is equal to the value of `g` at `a`, then `f` and `g` are the same continuous map. In other words, two continuous maps are equal if they agree on all points of their domain.
More concisely: If two continuous functions from one topological space to another agree on all points, then they are equal.
|
ContinuousMapClass.map_continuous
theorem ContinuousMapClass.map_continuous :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : FunLike F α β] [self : ContinuousMapClass F α β] (f : F), Continuous ⇑f
This theorem, `ContinuousMapClass.map_continuous`, states that for any types `F`, `α`, and `β`, where `α` and `β` are topological spaces, and `F` is a function-like type from `α` to `β` (i.e., instances of `F` can be treated as functions from `α` to `β`), if a `ContinuousMapClass` instance exists for `F`, `α`, and `β`, then any term `f` of type `F` is continuous. In mathematical terms, this means that if `f` is a map from a topological space `α` to another topological space `β` and `f` is a member of a class of maps known to be continuous, then the function `f` is indeed continuous.
More concisely: If `F` is a function-like type from topological spaces `α` to `β` with a `ContinuousMapClass` instance and `f : F` is a continuous map, then `f` is a continuous function from `α` to `β`.
|
ContinuousMap.coe_injective
theorem ContinuousMap.coe_injective :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
Function.Injective DFunLike.coe
The theorem `ContinuousMap.coe_injective` states that for any two types `α` and `β`, given the topology on both, the function `DFunLike.coe`, which is a coercion from some type `F` to a function, is injective. In other words, if two continuous maps from a topological space `α` to another topological space `β` are the same as functions (i.e., they map any element of `α` to the same element of `β`), then they are the same continuous maps.
More concisely: If two functions between topological spaces, when considered as continuous maps, are equal as functions, then they are equal as continuous maps.
|
ContinuousMap.continuousAt
theorem ContinuousMap.continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : C(α, β)) (x : α),
ContinuousAt (⇑f) x
This theorem states that for any topological spaces `α` and `β`, any continuous function `f` from `α` to `β`, and any point `x` in `α`, the function `f` is continuous at the point `x`. In other words, the output of the function `f` tends to the value `f(x)` as the input tends towards the point `x`. This theorem is deprecated and it's recommended to use `map_continuousAt` instead.
More concisely: For any topological spaces `α`, `β` and a continuous function `f` from `α` to `β`, `f` is continuous at any point `x` in `α`, meaning for any open set `U` in `β` containing `f(x)`, there exists an open set `V` in `α` containing `x` such that `f(V)` is contained in `U`.
|
Homeomorph.symm_comp_toContinuousMap
theorem Homeomorph.symm_comp_toContinuousMap :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
f.symm.toContinuousMap.comp f.toContinuousMap = ContinuousMap.id α
This theorem states that for any homeomorphism `f` from a topological space `α` to another topological space `β`, the composition of the continuous map corresponding to the inverse of `f` and the continuous map corresponding to `f` itself equals the identity continuous map on `α`. In other words, if you first apply `f` and then its inverse, you end up exactly where you started. This is a fundamental property of homeomorphisms and mirrors the property of inverses in group theory, specifically the property that the product of an element and its inverse equals the identity element.
More concisely: For any homeomorphism $f:\alpha \rightarrow \beta$, the inverse $f^{-1}$ satisfies $f \circ f^{-1} = id_\alpha$, where $id_\alpha$ is the identity map on $\alpha$.
|
ContinuousMap.continuous
theorem ContinuousMap.continuous :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : C(α, β)),
Continuous ⇑f
This theorem states that for any continuous function `f` between two topological spaces `α` and `β`, the application of `f` is a continuous operation. However, this theorem is deprecated and it is recommended to use `map_continuous` instead. In mathematical terminology, if `f` belongs to the set of continuous functions `C(α, β)` from `α` to `β`, then the operation `⇑f`, i.e., applying `f`, is continuous. Both `α` and `β` are arbitrary types equipped with a topological structure.
More concisely: If `f` is a continuous function between topological spaces `α` and `β`, then the application of `f` is a continuous function from `α` to `β`.
|
Homeomorph.toContinuousMap_comp_symm
theorem Homeomorph.toContinuousMap_comp_symm :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
f.toContinuousMap.comp f.symm.toContinuousMap = ContinuousMap.id β
This theorem states that for any homeomorphism `f` from a topological space `α` to another topological space `β`, the composition of the continuous map associated with `f` and the continuous map associated with the inverse of `f` is the identity continuous map on `β`. In other words, the inverse of a continuous map from a homeomorphism gives us back the original point in `β`, which is a property analogous to the property `Equiv.self_comp_symm` of equivalences.
More concisely: For any homeomorphism `f` between topological spaces `α` and `β`, the continuous maps `f.continuous` and `f⁻¹.continuous` satisfy `f.continuous ∘ f⁻¹.continuous = idβ`, where `idβ` is the identity map on `β`.
|
QuotientMap.lift_comp
theorem QuotientMap.lift_comp :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : C(X, Y)} (hf : QuotientMap ⇑f) (g : C(X, Z))
(h : Function.FactorsThrough ⇑g ⇑f), (hf.lift g h).comp f = g
The theorem `QuotientMap.lift_comp` states that for any three topological spaces `X`, `Y`, and `Z`, a continuous map `f` from `X` to `Y`, and another continuous map `g` from `X` to `Z`, if `f` is a quotient map and `g` factors through `f`, then the composition of the continuous map derived from "lifting" `g` along `f` and `f` itself is equal to `g`. This property can be visualized as a commutative triangle where the path from `X` to `Z` via `Y` using `f` and the lifted map is equivalent to the direct path from `X` to `Z` using `g`.
More concisely: If `f: X → Y` is a quotient map, `g: X → Z` is continuous and factors through `f`, then the lifted composition `g' ∘ f` equals `g`, where `g': Y → Z` is the unique continuous map such that `g' ∘ f = g`.
|
ContinuousMap.congr_arg
theorem ContinuousMap.congr_arg :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : C(α, β)) {x y : α},
x = y → f x = f y
This theorem is deprecated and it's recommended to use `DFunLike.congr_arg` instead. The theorem `ContinuousMap.congr_arg` states that for any two given types `α` and `β`, where `α` and `β` are topological spaces, and for a continuous function `f` from `α` to `β`, if two elements `x` and `y` in `α` are equal, then their images under the function `f`, namely `f(x)` and `f(y)`, are also equal. In other words, this theorem shows the congruence of arguments for a continuous map between two topological spaces.
More concisely: For any continuous function between topological spaces, if two elements are equal, then their images under the function are equal.
|
ContinuousMap.congr_fun
theorem ContinuousMap.congr_fun :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : C(α, β)},
f = g → ∀ (x : α), f x = g x
This theorem, `ContinuousMap.congr_fun`, states that for any two continuous functions `f` and `g` from a topological space `α` to another topological space `β`, if `f` and `g` are the same function (i.e., `f = g`), then the outputs of `f` and `g` for any given input `x` from `α` are the same (i.e., `f x = g x`). This theorem has been deprecated and it is recommended to use `DFunLike.congr_fun` instead.
More concisely: For any continuous functions `f` and `g` from a topological space `α` to another topological space `β`, if `f` is equal to `g`, then `f x = g x` for all `x` in `α`.
|
ContinuousMap.continuous_toFun
theorem ContinuousMap.continuous_toFun :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (self : C(α, β)),
Continuous self.toFun
This theorem states that for any two types `α` and `β` with corresponding topological spaces, the function `toFun` (which likely maps elements of type `α` to elements of type `β`) is continuous. Essentially, this means that if we have a continuous map from `α` to `β`, then the underlying function of that map is also continuous.
More concisely: Given types `α` and `β` with corresponding topological spaces, the function `toFun` from `α` to `β` is continuous if and only if the underlying function of any continuous map from `α` to `β` is `toFun`.
|