ContinuousMap.continuous_eval_const
theorem ContinuousMap.continuous_eval_const :
∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (a : X),
Continuous fun f => f a
The theorem `ContinuousMap.continuous_eval_const` states that for given topological spaces `X` and `Y`, and a point `a` of type `X`, the evaluation of any continuous map `f` from `X` to `Y` at the point `a` is itself a continuous function. In other words, if `f` varies over all continuous functions from `X` to `Y`, then the function which to `f` assigns `f(a)` is continuous. This is a fundamental property used in the study of topological spaces and continuous functions.
More concisely: For any topological spaces X and Y and continuous map f : X -> Y, the evaluation function x => f x of f at a point a in X is a continuous function.
|
ContinuousMap.continuous_comp'
theorem ContinuousMap.continuous_comp' :
∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] [inst_3 : LocallyCompactPair Y Z], Continuous fun x => x.2.comp x.1
This theorem states that, given three topological spaces X, Y, Z and assuming that Y is locally compact, the composition operation is continuous when considering the space of continuous maps from X to Y and from Y to Z, i.e., it defines a continuous map from the pair of continuous maps (`C(X, Y)`, `C(Y, Z)`) to `C(X, Z)`. In other words, composing two continuous maps yields a continuous map. This fact is Proposition 9 from Chapter X, Section 3, Number 4 of Bourbaki's "General Topology".
More concisely: The composition of two continuous functions between topological spaces is a continuous function.
|
ContinuousMap.continuous_curry'
theorem ContinuousMap.continuous_curry' :
∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (f : C(X × Y, Z)), Continuous f.curry'
This theorem states that for any types `X`, `Y`, and `Z`, each equipped with a topological space structure, if a function `f` is defined to map points from the product space `X × Y` to `Z` (represented by `C(X × Y, Z)`) and `f` is continuous, then the curried form of `f` (represented by `f.curry'`), which maps points from `X` to the space of continuous functions from `Y` to `Z`, is also continuous. Basically, it's a formal statement of the fact that curry operations preserve continuity in a topological context.
More concisely: If `f : X × Y → Z` is a continuous function, then its curried form `f.curry : X → C(Y, Z)` is also continuous.
|
ContinuousMap.continuous_comp
theorem ContinuousMap.continuous_comp :
∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (g : C(Y, Z)), Continuous g.comp
The theorem `ContinuousMap.continuous_comp` states that for any three types `X`, `Y`, and `Z` (representing topological spaces), and for any continuous map `g` from `Y` to `Z` (denoted as `C(Y, Z)`), the composition operation `ContinuousMap.comp g` is a continuous function. In other words, `C(X, ·)` is a functor - it preserves the structure between the topological spaces. In terms of mathematics, if we have two continuous functions `f` and `g`, the composition of these functions `(g ∘ f)` is also a continuous function.
More concisely: The theorem `ContinuousMap.continuous_comp` asserts that the composition of two continuous functions between topological spaces is a continuous function.
|
ContinuousMap.continuous_restrict
theorem ContinuousMap.continuous_restrict :
∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set X),
Continuous fun F => ContinuousMap.restrict s F
This theorem states that for any subset `s` of a topological space `X`, the operation of restricting continuous functions from `X` to `Y` to the subset `s` is itself a continuous operation. In other words, given any two topological spaces `X` and `Y` and a subset `s` of `X`, the map that sends a continuous function between `X` and `Y` to its restriction to `s` (still a continuous function) is a continuous map between the space of continuous functions `X → Y` and `s → Y`, where both function spaces are endowed with their respective compact-open topologies.
More concisely: The restriction of continuous functions from a topological space X to Y to a subset s of X is a continuous map from the space of continuous functions X -> Y to the space of continuous functions s -> Y with respect to the compact-open topologies.
|
ContinuousMap.compactOpen_eq_sInf_induced
theorem ContinuousMap.compactOpen_eq_sInf_induced :
∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
ContinuousMap.compactOpen =
⨅ K, ⨅ (_ : IsCompact K), TopologicalSpace.induced (ContinuousMap.restrict K) ContinuousMap.compactOpen
This theorem states that the compact-open topology on the space of continuous maps between two topological spaces `X` and `Y`, denoted as `C(X, Y)`, is equal to the infimum of the compact-open topologies on `C(s, Y)` for `s` being a compact subset of `X`. This is based on the key point that for any compact set `K`, the universal set `Set.univ : Set K` is also a compact set. In other words, the approach to understanding the compact-open topology on the function space `C(X, Y)` is via the induced topologies on the restrictions of these functions to the compact subsets of `X`.
More concisely: The compact-open topology on the space of continuous functions from a topological space `X` to `Y` equals the inference of the compact-open topologies on the subspaces of `C(X, Y)` consisting of functions with compact domain in `X`.
|
ContinuousMap.continuous_comp_left
theorem ContinuousMap.continuous_comp_left :
∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (f : C(X, Y)), Continuous fun g => g.comp f
The theorem `ContinuousMap.continuous_comp_left` states that for any topological spaces `X`, `Y`, and `Z`, and for any continuous function `f` from `X` to `Y`, the function that maps any continuous function `g` from `Y` to `Z` to the composition of `g` and `f` (i.e., `ContinuousMap.comp g f`) is also continuous. In other words, the "composition with `f` on the left" operation is continuous. This means that the space of continuous functions `C(·, Z)` behaves as a functor in the category of topological spaces.
More concisely: The composition of a continuous function with another continuous function, evaluated from the left, is a continuous function.
|
ContinuousMap.continuous_eval'
theorem ContinuousMap.continuous_eval' :
∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : LocallyCompactPair X Y], Continuous fun p => p.1 p.2
This theorem states that for any types `X` and `Y`, if `X` and `Y` form a locally compact pair of spaces (i.e., each point in the space has a compact neighborhood), then the evaluation map, which takes a pair consisting of a continuous map from `X` to `Y` and a point in `X` and returns the image of the point under the map, is continuous.
More concisely: Given locally compact spaces X and Y, the evaluation map from the space of continuous functions X -> Y to Y x X is continuous.
|
ContinuousMap.continuous_eval
theorem ContinuousMap.continuous_eval :
∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : LocallyCompactPair X Y], Continuous fun p => p.1 p.2
This theorem states that for any pair of types `X` and `Y`, where `X` and `Y` are both topological spaces and form a locally compact pair, the evaluation map from the Cartesian product of the set of continuous maps from `X` to `Y` and `X` to `Y` is continuous. In mathematical terms, if we consider `C(X, Y)` to be the set of continuous maps from `X` to `Y`, then the map `(f, x) ↦ f(x)` is continuous under the given conditions.
More concisely: Given topological spaces X and Y forming a locally compact pair, the evaluation map from the set of continuous functions C(X, Y) to Y^X (the set of all functions from X to Y) defined by (f, x) ↦ f(x) is continuous.
|
ContinuousMap.continuous_uncurry_of_continuous
theorem ContinuousMap.continuous_uncurry_of_continuous :
∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] [inst_3 : LocallyCompactSpace Y] (f : C(X, C(Y, Z))),
Continuous (Function.uncurry fun x y => (f x) y)
This theorem states that for any three types `X`, `Y`, and `Z` with each being a topological space and `Y` being a locally compact space, if there is a continuous map `f` from `X` to the space of continuous functions from `Y` to `Z` (denoted as `C(Y, Z)`), then the uncurried form of this map - which can be interpreted as a function mapping a pair `(x, y)` to `Z` by first applying `f` to `x` to get a function, and then applying this function to `y` - is also continuous. In other words, a continuous map from `X` to `C(Y, Z)` can be transformed into a continuous map from the product space `X × Y` to `Z`.
More concisely: If `X`, `Y`, and `Z` are topological spaces with `Y` locally compact, and `f : X → C(Y, Z)` is continuous, then the uncurried function `g : X × Y → Z` defined by `g(x, y) = f(x)(y)` is continuous.
|
ContinuousMap.continuous_coe
theorem ContinuousMap.continuous_coe :
∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Continuous DFunLike.coe
This theorem states that for all types `X` and `Y`, given that `X` and `Y` are both topological spaces, the coercion from type `C(X, Y)` (where 'C' represents collections of continuous functions between `X` and `Y` with the compact-open topology) to type `X → Y` (representing functions from `X` to `Y` with the pointwise convergence topology) is a continuous map. This is essentially stating that the process of coercion preserves the topological structure, which is crucial in the study of topological spaces. The note also mentions that this theorem is a port of two previously separate theorems, `continuous_coe` and `continuous_coe'`, where some unnecessary assumptions have been removed.
More concisely: The coercion from the type of continuous functions between topological spaces X and Y with compact-open topology to the type of functions from X to Y with pointwise convergence topology is a continuous map.
|
ContinuousMap.isOpen_setOf_mapsTo
theorem ContinuousMap.isOpen_setOf_mapsTo :
∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {K : Set X} {U : Set Y},
IsCompact K → IsOpen U → IsOpen {f | Set.MapsTo (⇑f) K U}
The theorem `ContinuousMap.isOpen_setOf_mapsTo` states that for any types `X` and `Y` that are equipped with topological space structures, and for any sets `K` of type `X` and `U` of type `Y`, if `K` is compact and `U` is open, then the set of all continuous maps `f` such that the image of `K` under `f` is contained in `U`, is an open set. In other words, the set of all continuous functions that map a compact set to an open set is itself an open set in the function space.
More concisely: The set of continuous functions from a compact topological space to an open subset of another topological space is an open subset in the function space.
|
ContinuousMap.compactOpen_eq
theorem ContinuousMap.compactOpen_eq :
∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
ContinuousMap.compactOpen =
TopologicalSpace.generateFrom
(Set.image2 (fun K U => {f | Set.MapsTo (⇑f) K U}) {K | IsCompact K} {t | IsOpen t})
The theorem `ContinuousMap.compactOpen_eq` states that for any types `X` and `Y` equipped with topological spaces, the compact-open topology on the space of continuous maps from `X` to `Y` is the smallest topological space containing the collection of sets formed by the image of the binary function `{f | Set.MapsTo (⇑f) K U}`, where `K` is a set which is compact and `U` is a set which is open. This binary function consists of all maps `f` that map each element of `K` to an element of `U`. Thus, the theorem characterizes the compact-open topology in terms of basic sets given by mappings of compact sets into open sets.
More concisely: The compact-open topology on the space of continuous maps from a compact set in X to an open set in Y is the smallest topology making all images of compact sets under continuous maps open.
|
ContinuousMap.embedding_comp
theorem ContinuousMap.embedding_comp :
∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (g : C(Y, Z)), Embedding ⇑g → Embedding g.comp
The theorem `ContinuousMap.embedding_comp` states that if `g` is a continuous function from a topological space `Y` to another topological space `Z` that is a topological embedding (i.e., `g` is an injective function that preserves the topology), then the composition of `g` with any continuous function from a topological space `X` to `Y` is also a topological embedding. In simpler terms, if a function `g` embeds one space into another, then composing `g` with another function also results in an embedding.
More concisely: If `g : Y �� /******/-> Z` is a continuous, injective topological embedding, then the composition `g ∘ f : X �� /******/-> Z` is a topological embedding for any continuous function `f : X �� /******/-> Y`.
|
ContinuousMap.continuous_uncurry
theorem ContinuousMap.continuous_uncurry :
∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] [inst_3 : LocallyCompactSpace X] [inst_4 : LocallyCompactSpace Y],
Continuous ContinuousMap.uncurry
The theorem `ContinuousMap.continuous_uncurry` states that for any given types `X`, `Y`, and `Z` - where `X`, `Y`, and `Z` are topological spaces and `X`, `Y` are locally compact spaces - the uncurrying process, represented by `ContinuousMap.uncurry`, is a continuous map between these function spaces. In mathematical terms, this means the operation of transforming a function that takes multiple arguments into a function that takes a single argument (a tuple of the original arguments) maintains the property of continuity.
More concisely: The uncurrying function `ContinuousMap.uncurry` is a continuous map between the spaces of continuous functions from a product of two locally compact topological spaces to a third topological space.
|
ContinuousMap.inducing_comp
theorem ContinuousMap.inducing_comp :
∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (g : C(Y, Z)), Inducing ⇑g → Inducing g.comp
The theorem states that for any three types `X`, `Y`, `Z`, each equipped with a topological space structure, if a continuous map `g` from `Y` to `Z` induces the topology on `Z`, then the composition of `g` with any continuous map from `X` to `Y` also induces the topology on `Z`. In other words, if `g` is a topology inducing map, the composition of `g` with any other continuous map is also a topology inducing map.
More concisely: If `g : Y → Z` is a continuous map that induces the topology on `Z`, then the composition `g ∘ f` induces the topology on `Z` for any continuous map `f : X → Y`.
|
ContinuousMap.continuous_curry
theorem ContinuousMap.continuous_curry :
∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] [inst_3 : LocallyCompactSpace (X × Y)], Continuous ContinuousMap.curry
The theorem `ContinuousMap.continuous_curry` states that for any three types `X`, `Y`, and `Z` (which are representing spaces) with the condition that each type has a topology and the product space of `X` and `Y` is locally compact, the process of currying (transforming a function that takes multiple arguments into a function that takes a single argument and returns another function) is a continuous mapping. In other words, this theorem is saying that the currying operation preserves the continuity of functions in these topological spaces.
More concisely: The currying operation preserves continuity for functions between locally compact topological spaces.
|
ContinuousMap.exists_tendsto_compactOpen_iff_forall
theorem ContinuousMap.exists_tendsto_compactOpen_iff_forall :
∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : WeaklyLocallyCompactSpace X] [inst_3 : T2Space Y] {ι : Type u_5} {l : Filter ι} [inst_4 : l.NeBot]
(F : ι → C(X, Y)),
(∃ f, Filter.Tendsto F l (nhds f)) ↔
∀ (s : Set X), IsCompact s → ∃ f, Filter.Tendsto (fun i => ContinuousMap.restrict s (F i)) l (nhds f)
The theorem `ContinuousMap.exists_tendsto_compact_open_iff_forall` states that for any topological spaces `X` and `Y`, where `X` is a weakly locally compact space, and `Y` is a Hausdorff space (or T2 space), given any filter `l` over an index set `ι` and a family of continuous functions `F` from `ι` to the set of continuous functions from `X` to `Y`, the family `F` converges in the compact-open topology to some function `f` if and only if for every compact subset `s` of `X`, the restriction of the function `F(i)` to `s` converges in the compact-open topology to some function `f`. Here, convergence is defined with respect to the filter `l` and in terms of the neighbourhood filter at `f`.
More concisely: A family of continuous functions from a weakly locally compact space to a Hausdorff space converges in the compact-open topology if and only if the restriction of each function to every compact subset converges in the compact-open topology to the same limit.
|
ContinuousMap.continuous_of_continuous_uncurry
theorem ContinuousMap.continuous_of_continuous_uncurry :
∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (f : X → C(Y, Z)),
Continuous (Function.uncurry fun x y => (f x) y) → Continuous f
The theorem `ContinuousMap.continuous_of_continuous_uncurry` states that for any types `X`, `Y`, and `Z` that are topological spaces, if you have a function `f` mapping from `X` to the continuous maps from `Y` to `Z` (`C(Y, Z)`), and you can show that the uncurried version of this function (which maps a pair of elements from `X` and `Y` to `Z`) is continuous, then the original function `f` is also continuous. In other words, to demonstrate the continuity of a function that outputs continuous functions, it's sufficient to show that the function's uncurried form is continuous.
More concisely: If `X`, `Y`, and `Z` are topological spaces, and `f : X → C(Y, Z)` is a function such that the uncurried version `\× → f x y` of `f` is continuous, then `f` is continuous.
|