continuous_inf_dom_right₂
theorem continuous_inf_dom_right₂ :
∀ {X : Type u_5} {Y : Type u_6} {Z : Type u_7} {f : X → Y → Z} {ta1 ta2 : TopologicalSpace X}
{tb1 tb2 : TopologicalSpace Y} {tc1 : TopologicalSpace Z},
(Continuous fun p => f p.1 p.2) → Continuous fun p => f p.1 p.2
This theorem, `continuous_inf_dom_right₂`, states that for any three types `X`, `Y`, and `Z`, and any binary function `f` from `X` to `Y` to `Z`, along with two topological spaces each on `X` and `Y` and one topological space on `Z`; if the function `f` is continuous when applied to a pair of elements (where the first element is from the type `X` and the second element is from the type `Y`), then the function `f` remains continuous when applied to another pair of elements (where again the first element is from the type `X` and the second element is from the type `Y`). Essentially, it says that the continuity of a binary function in a certain topological context is preserved under certain conditions.
More concisely: If a binary function between two topological spaces is continuous at every pair of points from their respective spaces, then it is continuous as a function between the product spaces.
|
Continuous.Prod.mk
theorem Continuous.Prod.mk :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X),
Continuous fun y => (x, y)
This theorem, `Continuous.Prod.mk`, states that for all types `X` and `Y`, given that `X` and `Y` are topological spaces, any function which takes a fixed element `x` from `X` and maps any element `y` from `Y` to the ordered pair `(x, y)`, is a continuous function. In other words, in the context of topology, holding one element constant in a pair and varying the other results in a continuous function.
More concisely: For any topological spaces X and Y, the function that maps x in X to the ordered pair (x, y) for all y in Y is a continuous function.
|
isOpen_sigma_iff
theorem isOpen_sigma_iff :
∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {s : Set (Sigma σ)},
IsOpen s ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
The theorem `isOpen_sigma_iff` states that for all types `ι` and `σ`, where `σ` is a function from `ι` to some type, and for each `i` in `ι`, there exists a topological space on `σ i`. Given a set `s` in the sigma type `Sigma σ`, the set `s` is open if and only if, for every `i` in `ι`, the preimage of `s` under the function `Sigma.mk i` is open.
In simpler terms, in the context of topology, the theorem is examining the open sets within a space that is a disjoint union of many spaces. It asserts that a set in this disjoint union is open if and only if each of its "slices" in the individual spaces that compose the union is open.
More concisely: A set in the disjoint union of topological spaces, each indexed by a type `ι`, is open if and only if the preimage of the set under the canonical projection function is open in each indexed space.
|
continuousAt_subtype_val
theorem continuousAt_subtype_val :
∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop} {x : Subtype p}, ContinuousAt Subtype.val x
The theorem `continuousAt_subtype_val` states that for any topological space `X` and any predicate `p` defined on `X`, the function `Subtype.val` is continuous at any point `x` of the subtype `p`. In mathematical terms, it means that as points in the subtype `p` approach `x`, their corresponding elements in `X` (obtained via `Subtype.val`) tend towards the element in `X` corresponding to `x`.
More concisely: For any topological space X and predicate p on X, the function Subtype.val is continuous at every point x in the subtype p.
|
nhdsSet_prod_le
theorem nhdsSet_prod_le :
∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set X) (t : Set Y),
nhdsSet (s ×ˢ t) ≤ nhdsSet s ×ˢ nhdsSet t
This theorem states that for any pair of sets `s` and `t` in topological spaces `X` and `Y` respectively, the neighborhood filter of the product set `s ×ˢ t` is less than or equal to the product of the neighborhood filters of `s` and `t`. This is a statement about the relationship between neighborhood filters in product topological spaces, and it's phrased in terms of a filter inequality. This theorem is important in the study of continuity and convergence in product spaces.
More concisely: The neighborhood filter of a product set in product topological spaces is contained in the product of the neighborhood filters of its components.
|
Inducing.prod_map
theorem Inducing.prod_map :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : X → Y} {g : Z → W},
Inducing f → Inducing g → Inducing (Prod.map f g)
The theorem `Inducing.prod_map` states that for any four types `X`, `Y`, `Z`, and `W`, equipped with topological spaces, given two functions `f : X → Y` and `g : Z → W`, if `f` is an inducing function and `g` is also an inducing function, then the function `Prod.map f g`, which is defined on the Cartesian product of `X` and `Z` and maps each pair `(x, z)` to `(f(x), g(z))`, is also an inducing function. Here, an inducing function is one that induces (pulls back) the topology of its codomain to its domain.
More concisely: If functions `f : X → Y` and `g : Z → W` are inducing functions on topological spaces `X × Z`, then their composition `Prod.map f g : X × Z → Y × W` is also an inducing function.
|
Continuous.fst'
theorem Continuous.fst' :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : X → Z}, Continuous f → Continuous fun x => f x.1
The theorem `Continuous.fst'` states that, for any three types `X`, `Y`, and `Z` equipped with a topological space structure, and for any function `f` from `X` to `Z`, if `f` is continuous then the function obtained by precomposing `f` with the first projection function (`Prod.fst`) is also continuous. In other words, if `f` is a continuous function, then applying `f` to the first element of a pair of values (an element of the product type `X × Y`) results in a continuous function.
More concisely: If `f : X → Z` is continuous and `X` is a topological space, then the composed function `f ∘ Prod.fst : X × Y → Z` is continuous.
|
Continuous.codRestrict
theorem Continuous.codRestrict :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
Continuous f → ∀ (hs : ∀ (a : X), f a ∈ s), Continuous (Set.codRestrict f s hs)
This theorem states that given two types `X` and `Y`, each equipped with a topological structure, a function `f` from `X` to `Y`, and a subset `s` of `Y`, if `f` is a continuous function such that for every element `a` in `X`, `f(a)` is in `s`, then the codomain-restricted function `Set.codRestrict f s hs` is also continuous. In simple terms, if a function is continuous and its output always falls within a certain set, then even when we restrict the function's codomain to that set, the resulting function remains continuous.
More concisely: If `f : X → Y` is a continuous function and `s ⊆ Y` is such that `∀ x ∈ X, f x ∈ s`, then `Set.codRestrict f s` is a continuous function.
|
set_pi_mem_nhds
theorem set_pi_mem_nhds :
∀ {ι : Type u_5} {π : ι → Type u_6} [T : (i : ι) → TopologicalSpace (π i)] {i : Set ι} {s : (a : ι) → Set (π a)}
{x : (a : ι) → π a}, i.Finite → (∀ a ∈ i, s a ∈ nhds (x a)) → i.pi s ∈ nhds x
The theorem `set_pi_mem_nhds` states that for any type `ι`, any function `π` mapping `ι` to a type, any topological space `T` over each `π i`, any set `i` of type `ι`, any function `s` mapping each `ι` to a set of `π a`, and any function `x` mapping each `ι` to `π a`, if the set `i` is finite and for each element `a` in `i`, `s a` is a neighborhood of `x a`, then the set of all dependent functions such that `f a` belongs to `s a` whenever `a` is in `i` is a neighborhood of `x`. In more mathematical terms, this theorem states that the product of a finite number of neighborhoods of points is a neighborhood of the point in the product space.
More concisely: Given a topological space over a finite index type, if each index has a neighborhood containing the image of a function, then the product of these neighborhoods is a neighborhood of the function.
|
Filter.Eventually.prod_nhds
theorem Filter.Eventually.prod_nhds :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {q : Y → Prop}
{x : X} {y : Y},
(∀ᶠ (x : X) in nhds x, p x) → (∀ᶠ (y : Y) in nhds y, q y) → ∀ᶠ (z : X × Y) in nhds (x, y), p z.1 ∧ q z.2
The theorem `Filter.Eventually.prod_nhds` states that for any two types `X` and `Y` with topological space structures, given predicates `p` and `q` on `X` and `Y` respectively, and points `x` in `X` and `y` in `Y`, if all points sufficiently close to `x` (in the sense of the neighborhood filter) satisfy predicate `p`, and all points sufficiently close to `y` satisfy predicate `q`, then all points sufficiently close to the pair `(x, y)` (in the Cartesian product topology) will satisfy both `p` on the first component and `q` on the second component. That is, neighborhood properties of individual points extend naturally to the product topology.
More concisely: For any topological spaces X and Y, and points x in X and y in Y with predicates p on X and q on Y such that p holds for all points near x and q holds for all points near y, the predicates p and q hold for all points near the pair (x, y) in the product topology.
|
continuous_subtype_val
theorem continuous_subtype_val : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop}, Continuous Subtype.val := by
sorry
The theorem `continuous_subtype_val` states that for any type `X` equipped with a topological space structure, and any predicate `p` on `X`, the function `Subtype.val` is continuous. In other words, when we look at the subset of `X` defined by the predicate `p` as a subspace, the function which takes an element of the subset and returns the corresponding element of `X` preserves the topology: the preimage of any open subset of `X` is an open subset of the subspace.
More concisely: The function `Subtype.val` is continuous from the subspace topology on the subtype given by a predicate `p` on a topological space `X` to `X`.
|
nhds_prod_eq
theorem nhds_prod_eq :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x : X} {y : Y},
nhds (x, y) = nhds x ×ˢ nhds y
This theorem states that for any two types X and Y which both have a topological space structure, and for any elements x of X and y of Y, the neighborhood filter of the pair (x, y) in the product topology is equal to the product of the neighborhood filter of x and the neighborhood filter of y. This theorem is a fundamental property of product topologies in topology.
More concisely: For any topological spaces X and Y, and any x in X and y in Y, the neighborhood filter of the pair (x, y) in the product topology is equal to the product of the neighborhood filters of x in X and y in Y.
|
continuous_apply
theorem continuous_apply :
∀ {ι : Type u_5} {π : ι → Type u_6} [T : (i : ι) → TopologicalSpace (π i)] (i : ι), Continuous fun p => p i := by
sorry
This theorem states that for any index type `ι` and any type function `π` from `ι` to another type, given that each type `π i` is endowed with a topological space structure, the function that applies an element of `ι` to a point `p` (thus obtaining an element of type `π i`) is continuous. In other words, it's saying that projection maps in a product of topological spaces are continuous.
More concisely: For any index type `ι` and type function `π : ι → Type`, if each `π i` is endowed with a topological space structure, then the projection map `π` is continuous.
|
IsOpenMap.prod
theorem IsOpenMap.prod :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : X → Y} {g : Z → W},
IsOpenMap f → IsOpenMap g → IsOpenMap fun p => (f p.1, g p.2)
The theorem `IsOpenMap.prod` states that for any four types `X`, `Y`, `Z`, and `W` that each are topological spaces, given two functions `f : X → Y` and `g : Z → W` that are open maps (meaning that the image of any open set in `X` or `Z` is open in `Y` or `W` respectively), the function that takes a pair of points from `X` and `Z` and maps them to a pair in `Y` and `W` using `f` and `g` respectively, is also an open map.
More concisely: Given two open maps `f : X → Y` and `g : Z → W` between topological spaces `X`, `Y`, `Z`, and `W`, the function `(f, g) : X × Z → Y × W` that maps `(x, z)` to `(f(x), g(z))` is an open map.
|
Continuous.quotient_liftOn'
theorem Continuous.quotient_liftOn' :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Setoid X} {f : X → Y},
Continuous f → ∀ (hs : ∀ (a b : X), Setoid.r a b → f a = f b), Continuous fun x => x.liftOn' f hs
The theorem `Continuous.quotient_liftOn'` states that for any types `X` and `Y` endowed with topological spaces, a setoid `s` on `X`, and a continuous function `f` from `X` to `Y`, if `f` respects the equivalence relation of the setoid (i.e., `f` maps equivalent elements to the same element), then the function defined by lifting `f` to the quotient of `X` by the setoid, `Quotient.liftOn' x f hs`, is also continuous. This is essentially stating a property about the preservation of continuity under the operation of taking quotients by an equivalence relation.
More concisely: If `f : X → Y` is a continuous function between topological spaces `X` and `Y`, respecting the equivalence relation of a setoid `s` on `X`, then the function `Quotient.liftOn' x f hs` obtained by lifting `f` to the quotient `X/s` is also continuous.
|
isOpenMap_inr
theorem isOpenMap_inr :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsOpenMap Sum.inr
The theorem `isOpenMap_inr` states that for any two types `X` and `Y`, each equipped with a topological space structure, the injective function `Sum.inr`, which maps an element of `Y` into the right component of the sum type `X + Y`, is an open map. In other words, the image of any open set in `Y` under `Sum.inr` is an open set in the sum type `X + Y`.
More concisely: The injective function `Sum.inr` from a topological space `Y` to the sum type `X + Y` preserves open sets, that is, the image of any open set in `Y` is an open set in `X + Y`.
|
embedding_inclusion
theorem embedding_inclusion :
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X} (h : s ⊆ t), Embedding (Set.inclusion h)
The theorem `embedding_inclusion` states that for any type `X` equipped with a topological space structure, and for any two subsets `s` and `t` of `X` such that `s` is a subset of `t`, the inclusion function from `s` to `t` is an embedding. In other words, it asserts that the function that maps each element of the subset `s` to itself within the larger set `t` preserves the topological structure, implying that the subset `s` carries the subspace topology induced from `t`.
More concisely: For any topological space `(X, τ)` and subsets `s ⊆ t ⊆ X`, the inclusion function `i : s → t` is a continuous function, making `s` a subspace of `t` with the subspace topology.
|
Pi.continuous_postcomp'
theorem Pi.continuous_postcomp' :
∀ {ι : Type u_5} {π : ι → Type u_6} [T : (i : ι) → TopologicalSpace (π i)] {X : ι → Type u_8}
[inst : (i : ι) → TopologicalSpace (X i)] {g : (i : ι) → π i → X i},
(∀ (i : ι), Continuous (g i)) → Continuous fun f i => g i (f i)
This theorem states that given an indexed type `ι` and two families of types `π` and `X` indexed by `ι`, where each type in both families (`π` and `X`) has an associated topological space, and a family of functions `g` that maps each type in `π` to its corresponding type in `X`, if each function in the `g` family is continuous, then the composite function which applies `g` after `f` for each index `i` is also continuous. In mathematical terms, for each `i` in `ι`, if `g_i: π_i -> X_i` is continuous, then the function `(f -> g(f(i))) : (Πi, π_i) -> (Πi, X_i)` is also continuous.
More concisely: If, for each index `i`, the function `g_i: π_i -> X_i` is continuous, then the function `(λf. g (f i)): ∏i. π_i -> ∏i. X_i` is continuous.
|
IsOpen.prod
theorem IsOpen.prod :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
IsOpen s → IsOpen t → IsOpen (s ×ˢ t)
The theorem `IsOpen.prod` states that for any two types `X` and `Y` with their respective topological spaces, if `s` is an open set in the topological space of `X` and `t` is an open set in the topological space of `Y`, then the Cartesian product of `s` and `t` (denoted as `s ×ˢ t`) is also an open set in the product topological space. This theorem extends the concept of open sets to product spaces in topology.
More concisely: The Cartesian product of two open sets in the product topology is an open set.
|
continuous_sigmaMk
theorem continuous_sigmaMk :
∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {i : ι}, Continuous (Sigma.mk i) := by
sorry
This theorem states that for any index type `ι`, any family `σ` of types indexed by `ι`, and any index `i` of type `ι`, if each type `σ i` in the family is equipped with a topological space structure, then the function `Sigma.mk i`, which constructs a sigma type (dependent sum type) instance from an element of type `σ i`, is continuous. In other words, the mapping from a point in the space `σ i` to the corresponding point in the sigma type is compatible with the topology.
More concisely: For any index type `ι`, any family of topological spaces `(σ i : ι → Type)`, and any function `σ : Π i, ι → σ i → Σ i (σ i)`, the evaluation map `ev : ∀ i, σ i × σ i → σ i` is continuous.
|
continuous_mulSingle
theorem continuous_mulSingle :
∀ {ι : Type u_5} {π : ι → Type u_6} [T : (i : ι) → TopologicalSpace (π i)] [inst : (i : ι) → One (π i)]
[inst_1 : DecidableEq ι] (i : ι), Continuous fun x => Pi.mulSingle i x
The theorem `continuous_mulSingle` states that for any type `ι`, a type-valued function `π : ι → Type`, where each `π i` for `i : ι` is a topological space, and has a defined "one", and `ι` has decidable equality, the function `Pi.mulSingle i x` is continuous in `x` for any `i : ι`. In other words, `Pi.mulSingle i x` defines a continuous function from `π i` to the product space over all `j : ι` of `π j` where the function is supported at `i`, equals `x` at `i`, and `1` elsewhere.
More concisely: For any type `ι` with decidable equality, and for each `i : ι` a topological space `π i` with a defined "one", the function `Pi.mulSingle : ι → Π (j : ι), π j → π i × ∏ (k : ι), k ≠ i → π k → π i × 1` is continuous in `x` for each `i : ι`, where `x : π i`.
|
continuous_sum_dom
theorem continuous_sum_dom :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : X ⊕ Y → Z},
Continuous f ↔ Continuous (f ∘ Sum.inl) ∧ Continuous (f ∘ Sum.inr)
The theorem `continuous_sum_dom` states that for all types `X`, `Y`, and `Z` where `X`, `Y`, and `Z` are topological spaces, a function `f` from the disjoint union of `X` and `Y` to `Z` is continuous if and only if both the composition of `f` with the injection from `X` into the disjoint union (`Sum.inl`), and the composition of `f` with the injection from `Y` into the disjoint union (`Sum.inr`), are continuous.
More concisely: A function from the disjoint union of topological spaces X and Y to Z is continuous if and only if its restrictions to the subspaces X and Y are continuous.
|
continuous_inl
theorem continuous_inl :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Continuous Sum.inl := by
sorry
This theorem states that for any two types `X` and `Y`, which have topological space structures (denoted by `inst` and `inst_1`), the injection function `Sum.inl` (which takes an element from `X` and injects it into the left component of the sum type `X + Y`) is continuous. In the context of topology, a function is continuous if the preimage of every open set is open.
More concisely: For any topological spaces `X` and `Y`, the injection function `Sum.inl : X → X + Y` is a continuous function.
|
closedEmbedding_subtype_val
theorem closedEmbedding_subtype_val :
∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop}, IsClosed {a | p a} → ClosedEmbedding Subtype.val := by
sorry
This theorem states that for any type `X` endowed with a topological structure, and any property `p` on `X`, if the set of elements in `X` that satisfy `p` is a closed set, then the function `Subtype.val` is a closed embedding. In other words, `Subtype.val` function, which extracts the underlying element from a subtype where the element satisfies the property `p`, preserves the topological structure when the property `p` defines a closed set.
More concisely: If a subtype of a topological space, defined by a closed property, is a closed set, then its inclusion map is a closed embedding.
|
Mathlib.Topology.Constructions._auxLemma.7
theorem Mathlib.Topology.Constructions._auxLemma.7 :
∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsClosed s = IsOpen sᶜ
This theorem, named `Mathlib.Topology.Constructions._auxLemma.7`, states that for any type `X` and any set `s` of type `X` within a topological space (denoted by `inst : TopologicalSpace X`), the set `s` is closed if and only if the complement of `s` (denoted by `sᶜ`) is open. Here, `IsClosed s` and `IsOpen sᶜ` refer to the properties of the set being closed and the complement of the set being open in the given topological space, respectively.
More concisely: A set in a topological space is closed if and only if the complement of the set is open.
|
ContinuousAt.prod
theorem ContinuousAt.prod :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : X → Y} {g : X → Z} {x : X},
ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun x => (f x, g x)) x
The theorem `ContinuousAt.prod` states that for all types `X`, `Y`, and `Z` with `X` as the input type and `Y` and `Z` as output types where `X`, `Y`, and `Z` are topological spaces, for any two functions `f : X → Y` and `g : X → Z` and a point `x` in `X`, if the functions `f` and `g` are continuous at the point `x`, then the function that maps `x` to the ordered pair `(f x, g x)` is also continuous at `x`. In other words, the product of two continuous functions at a particular point is also continuous at that point.
More concisely: If functions `f : X → Y` and `g : X → Z` are continuous at a point `x` in a topological space `X`, then the function `(f, g) : X → Y × Z` defined by `(f, g) x = (f x, g x)` is continuous at `x`.
|
ContinuousAt.snd'
theorem ContinuousAt.snd' :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : Y → Z} {x : X} {y : Y},
ContinuousAt f y → ContinuousAt (fun x => f x.2) (x, y)
The theorem `ContinuousAt.snd'` states that for any three types `X`, `Y`, and `Z`, each equipped with a topological space structure, and for any function `f` from type `Y` to `Z`, along with any elements `x` of type `X` and `y` of type `Y`, if the function `f` is continuous at `y`, then the function that takes a pair `(x, y)` and applies `f` to the second element of the pair is also continuous at the point `(x, y)`. In mathematical terms, if $f : Y \rightarrow Z$ is continuous at a point $y \in Y$, then the function $g : X \times Y \rightarrow Z$ defined by $g(x, y) = f(y)$ is continuous at the point $(x, y)$.
More concisely: If a function between topological spaces is continuous at a point, then the function that takes a pair consisting of an element from the domain and the point, and applies the original function to the second element, is also continuous at that pair.
|
Continuous.prod_mk
theorem Continuous.prod_mk :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : Z → X} {g : Z → Y},
Continuous f → Continuous g → Continuous fun x => (f x, g x)
The theorem `Continuous.prod_mk` states that for any three types `X`, `Y`, and `Z` with each a topological space, given two functions `f : Z → X` and `g : Z → Y`, if `f` and `g` are continuous, then the function that takes an element of type `Z` and returns a pair with the first element mapped by `f` and the second element mapped by `g` is also continuous.
More concisely: If `f : Z -> X` and `g : Z -> Y` are continuous functions, then the function `h : Z -> X × Y` defined by `h x = (f x, g x)` is continuous.
|
continuousAt_fst
theorem continuousAt_fst :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X × Y},
ContinuousAt Prod.fst p
The theorem `continuousAt_fst` states that for all types `X` and `Y` that have a topological space structure, and for every pair `p` with elements from `X` and `Y`, the first projection function `Prod.fst`, which returns the first element of the pair, is continuous at the point `p`. In mathematical terms, this means that for any sequence of points in `X × Y` that converges to `p`, the sequence of their first components also converges to the first component of `p`.
More concisely: For every topological space `(X,τX)` and `(Y,τY)`, and every point `(pX, pY)` in their product `(X × Y, τX × τY)`, the first projection function `Prod.fst` is continuous at `(pX, pY)`, that is, for any convergent sequence `(x_n, y_n)` in `X × Y` with limit `(pX, pY)`, the sequence `x_n` converges to `pX` in `X`.
|
continuous_prod_mk
theorem continuous_prod_mk :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : X → Y} {g : X → Z},
(Continuous fun x => (f x, g x)) ↔ Continuous f ∧ Continuous g
This theorem states that for any three types `X`, `Y`, and `Z` where `X`, `Y`, and `Z` are equipped with topological spaces, given two functions `f : X → Y` and `g : X → Z`, the function that maps each element of `X` to the pair `(f(x), g(x))` in `Y × Z` is continuous if and only if both `f` and `g` are continuous. This is a fundamental result in topology which characterizes the continuity of product functions in terms of the continuity of their component functions.
More concisely: The function that maps each element of a topological space `X` to the pair of its images under continuous functions `f : X → Y` and `g : X → Z` is a continuous function from `X` to `Y × Z`. (If X, Y, Z are topological spaces and f and g are continuous functions.)
|
embedding_sigmaMk
theorem embedding_sigmaMk :
∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {i : ι}, Embedding (Sigma.mk i) := by
sorry
This theorem, `embedding_sigmaMk`, states that for any type `ι`, any function `σ` from `ι` to some type, and for any index `i` of type `ι`, the function `Sigma.mk i` is an embedding. Here, each `σ i` is equipped with a topology, making `σ i` a topological space for each `i` in `ι`. In this context, an embedding is a function that is both injective (or one-to-one) and continuous, with its image also being a closed set. The function `Sigma.mk i` creates a sigma type, essentially a tagged union, with the tag being `i`.
More concisely: For any type `ι`, function `σ : ι → X` with each `σ i` a topological space, and index `i : ι`, the function `Σ.mk i : σ i → Σ i × *, where Σ i is the sigma type over `ι` with tag `i`, is an injective and continuous embedding.
|
nhds_pi
theorem nhds_pi :
∀ {ι : Type u_5} {π : ι → Type u_6} [T : (i : ι) → TopologicalSpace (π i)] {a : (i : ι) → π i},
nhds a = Filter.pi fun i => nhds (a i)
This theorem, `nhds_pi`, states that for any type `ι`, any function `π` from `ι` to another type, a topology `T` on the type space `π i` for each `i` in `ι`, and any function `a` from `ι` to `π i`, the neighborhood filter at `a` is equal to the product of the neighborhood filters at each `a i`. In other words, the neighborhood of a point in a product space is the product of the neighborhoods of the components of that point. Here, a product space is a space obtained by taking the Cartesian product of a family of spaces, and the Cartesian product of a family of sets is the set of all possible sequences that can be formed by selecting one member from each of the sets in the family.
More concisely: For any function `π:` `ι` → Type, given topologies `T_i` on `π i` for each `i` in `ι`, and a function `a:` `ι` → `π i`, the neighborhood filter at `a` in the product space `∏ i, (π i, T_i)` is equal to the product of the neighborhood filters at `a i` in `(π i, T_i)`.
|
embedding_uLift_down
theorem embedding_uLift_down : ∀ {X : Type u} [inst : TopologicalSpace X], Embedding ULift.down
This theorem states that for every type `X` which has an instance of a Topological Space, the function `ULift.down` is an embedding. In mathematical terms, the function `ULift.down` is a homeomorphism from the topological space `ULift X` onto its image under `ULift.down`, which is a subset of `X`. An embedding is a function that preserves the topological structure, meaning the function and its inverse are both continuous. Here, `ULift.down` is such a function that extracts a value from an uplifted type `ULift α`, maintaining the topological structure.
More concisely: The function `ULift.down` is a homeomorphism between the topological space `ULift X` and its image in `X`.
|
Pi.continuous_precomp'
theorem Pi.continuous_precomp' :
∀ {ι : Type u_5} {π : ι → Type u_6} [T : (i : ι) → TopologicalSpace (π i)] {ι' : Type u_8} (φ : ι' → ι),
Continuous fun f j => f (φ j)
For all types `ι` and `π`, if `π` is a function from `ι` to a topology, and `φ` is a function from some other type `ι'` to `ι`, then the function which takes a function `f` and a value `j` and gives `f (φ j)` is continuous. Here, continuity is defined in the topological sense - that is, the preimage of every open set is open.
More concisely: Given a type `ι`, a function `π : ι → Topology`, and a function `φ : ι' → ι`, the function `f ↦ φ → f ∘ φ` is continuous from `(Fun ι' ι) → (OpenSet (π i))` to `(OpenSet (π i))`.
|
continuous_quot_mk
theorem continuous_quot_mk : ∀ {X : Type u} [inst : TopologicalSpace X] {r : X → X → Prop}, Continuous (Quot.mk r) := by
sorry
This theorem states that for any type `X` equipped with a topological space structure and for any equivalence relation `r` on `X`, the quotient map (`Quot.mk r`) that sends each element of `X` to its equivalence class in the quotient space `Quot r` is continuous. In other words, the preimage of any open set in the quotient space `Quot r` under this map is an open set in `X`. This is a fundamental property in topology, especially when dealing with the quotient spaces.
More concisely: Given a topological space `(X, τ)` and an equivalence relation `r` on `X`, the quotient map `Quot.mk r : X → Quot r` is a continuous function.
|
openEmbedding_sigmaMk
theorem openEmbedding_sigmaMk :
∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {i : ι}, OpenEmbedding (Sigma.mk i)
This theorem states that for any type `ι`, any type function `σ` mapping `ι` to another type, and a given instance of a topological space for each `σ i`, where `i` is an element of `ι`, the function `Sigma.mk i` that takes an element of `σ i` and constructs a sigma type is an open embedding. In topology, an open embedding is a function between topological spaces that is both an embedding and an open map, meaning it injectively maps points to points and open sets to open sets.
More concisely: For any type `ι`, given instances of topological spaces for each `σ i` where `i` is an element of `ι`, the function `Sigma.mk : ∀ i : ι, σ i → Σ i, σ i` is an open embedding.
|
Continuous.prod_map
theorem Continuous.prod_map :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : Z → X} {g : W → Y},
Continuous f → Continuous g → Continuous fun p => (f p.1, g p.2)
This theorem, `Continuous.prod_map`, asserts that for any four types `X`, `Y`, `Z`, `W`, given that `X`, `Y`, `Z`, `W` are equipped with topological spaces, and given two functions `f : Z → X` and `g : W → Y`, if `f` and `g` are continuous, then the function that takes a pair `(z, w)` and maps it to `(f(z), g(w))` is also continuous. This implies that the continuity of individual functions is preserved under the formation of product functions in topological spaces.
More concisely: If `f : Z → X` and `g : W → Y` are continuous functions between topological spaces, then the function `(z, w) ↦ (f(z), g(w))` from `Z × W` to `X × Y` is continuous.
|
Prod.tendsto_iff
theorem Prod.tendsto_iff :
∀ {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] {X : Type u_5}
(seq : X → Y × Z) {f : Filter X} (p : Y × Z),
Filter.Tendsto seq f (nhds p) ↔
Filter.Tendsto (fun n => (seq n).1) f (nhds p.1) ∧ Filter.Tendsto (fun n => (seq n).2) f (nhds p.2)
The `Prod.tendsto_iff` theorem states that for any types `Y` and `Z` with topological space structures, a type `X`, a sequence `seq` of function from `X` to the cartesian product of `Y` and `Z`, a filter `f` on `X`, and a pair `p` in `Y x Z`, the sequence `seq` tends to the neighborhood filter of `p` (i.e., the values of the sequence get arbitrarily close to `p`) if and only if both projections of the sequence (i.e., the first and second components of the pairs in the sequence), under the filter `f`, tend to the neighborhood filters of the first and the second components of `p`, respectively.
More concisely: For any types `Y` and `Z` with topological spaces structures, a sequence `seq` of functions from `X` to `Y × Z`, filter `f` on `X`, and point `p` in `Y × Z`, `seq` tends to the neighborhood filter of `p` if and only if the projections of `seq` do, under `f`.
|
tendsto_pi_nhds
theorem tendsto_pi_nhds :
∀ {Y : Type v} {ι : Type u_5} {π : ι → Type u_6} [T : (i : ι) → TopologicalSpace (π i)] {f : Y → (i : ι) → π i}
{g : (i : ι) → π i} {u : Filter Y},
Filter.Tendsto f u (nhds g) ↔ ∀ (x : ι), Filter.Tendsto (fun i => f i x) u (nhds (g x))
The theorem `tendsto_pi_nhds` states that for any type `Y`, indexing type `ι`, function type `π : ι → Type u_6`, where every `π i` is a topological space, and for any functions `f : Y → (i : ι) → π i` and `g : (i : ι) → π i`, and a filter `u` on `Y`, the function `f` tends to the neighborhood filter of `g` under the filter `u` if and only if, for every index `x` in `ι`, the function `f` composed with the constant function at `x` tends to the neighborhood filter of `g x` under filter `u`.
In essence, this theorem is about continuity of functions into product spaces in topology. It provides a condition for a function to be continuous at a certain point in terms of the function's behavior in each individual coordinate.
More concisely: For a function between topological spaces and a filter on the domain, the function tends to the neighborhood filter of a point in the codomain under the filter if and only if the composition of the function with the constant function at each index point tends to the neighborhood filter of the corresponding point in the codomain under the filter.
|
inducing_subtype_val
theorem inducing_subtype_val : ∀ {Y : Type v} [inst : TopologicalSpace Y] {t : Set Y}, Inducing Subtype.val
This theorem states that for any type `Y` equipped with a topological structure (`inst : TopologicalSpace Y`) and a set `t` of type `Y`, the function `Subtype.val` is an inducing function. In topology, an inducing function between two topological spaces is a function that generates the topology of the range space from the topology of the domain space. Here, the `Subtype.val` function, which retrieves the underlying element from a subtype, is such an inducing function. The topology on the subtype is thus the subspace topology inherited from `Y` via the `Subtype.val` function.
More concisely: The `Subtype.val` function is an inducing function for the subspace topology of a subtype in a topological space.
|
continuous_sigma_iff
theorem continuous_sigma_iff :
∀ {X : Type u} {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)]
[inst_1 : TopologicalSpace X] {f : Sigma σ → X}, Continuous f ↔ ∀ (i : ι), Continuous fun a => f ⟨i, a⟩
This theorem, `continuous_sigma_iff`, states that for any types `X`, `ι`, and a type family `σ` indexed by `ι`, given instances of topological spaces for each type `σ i` and for `X`, a function `f` from the sigma type of `σ` into `X` is continuous if and only if for each `i` in `ι`, the function `f` when restricted to the elements of `σ i` (the `i`'th summand of the sigma type) is continuous. In other words, a function mapping out of a sum type is continuous if and only if its restriction to each summand is continuous.
More concisely: A function from the sum type indexed by a topological space to a topological space is continuous if and only if the restriction of the function to each summand is continuous.
|
continuous_inr
theorem continuous_inr :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Continuous Sum.inr := by
sorry
This theorem states that for any types `X` and `Y` with respective topological spaces, the function `Sum.inr` is continuous. In the context of topology, `Sum.inr` is a function that takes an element of type `Y` and returns that element as part of a disjoint union (also known as a sum type) with `X`. The continuity of this function means that the preimage of any open set in the disjoint union is an open set in `Y`.
More concisely: The function `Sum.inr`: `Y → X ± Y` is continuous with respect to the subspace topology on `Y`, where `X ± Y` denotes the disjoint union of `X` and `Y`.
|
map_snd_nhdsWithin
theorem map_snd_nhdsWithin :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X × Y),
Filter.map Prod.snd (nhdsWithin x (Prod.fst ⁻¹' {x.1})) = nhds x.2
The theorem `map_snd_nhdsWithin` states that for any given point `x` in the product of spaces `X × Y` with `X` and `Y` being topological spaces, the operation of mapping the second projection `Prod.snd` over the "neighbourhood within" filter of `x` in the preimage of the first projection `Prod.fst` equals the neighbourhood filter at `x.2`. In simpler terms, it means that the neighborhood of the second component of `x` in the original space `Y` can be obtained by taking the filter of neighborhood of `x` within the section defined by keeping the first component constant, and then applying the map that projects onto the second component.
More concisely: The neighborhood filter of the second component of a point in the product space with respect to the product topology is equal to the image under the second projection of the neighborhood filter of that point in the product space, where the neighborhood filters are taken with respect to the subspace topologies on the factors.
|
frontier_prod_eq
theorem frontier_prod_eq :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set X) (t : Set Y),
frontier (s ×ˢ t) = closure s ×ˢ frontier t ∪ frontier s ×ˢ closure t
The theorem `frontier_prod_eq` states that for any two types `X` and `Y` equipped with topological structures, and any sets `s` of type `X` and `t` of type `Y`, the frontier (the set of points between the closure and interior) of the cartesian product of `s` and `t` is equal to the union of two sets: the cartesian product of the closure of `s` and the frontier of `t`, and the cartesian product of the frontier of `s` and the closure of `t`. In mathematical terms, this can be written as `Fr(s × t) = Cl(s) × Fr(t) ∪ Fr(s) × Cl(t)` where `Fr`, `Cl`, `×`, and `∪` represent the frontier, closure, cartesian product, and union operations respectively.
More concisely: The frontier of a cartesian product of sets equals the union of the product of the closure of each set and the frontier of the other, and the product of the frontiers and closures of each set.
|
Continuous.update
theorem Continuous.update :
∀ {X : Type u} {ι : Type u_5} {π : ι → Type u_6} [inst : TopologicalSpace X] [T : (i : ι) → TopologicalSpace (π i)]
{f : X → (i : ι) → π i} [inst_1 : DecidableEq ι],
Continuous f → ∀ (i : ι) {g : X → π i}, Continuous g → Continuous fun a => Function.update (f a) i (g a)
This theorem states that if we have a continuous function `f` from a topological space `X` to a dependent function type `(i : ι) → π i` where each `π i` is a topological space, and we have another continuous function `g` from `X` to one of the `π i`, then the function that updates the value of `f` at `i` with the value of `g` at the same point is also continuous.
The updating operation is carried out using the `Function.update` function, which replaces the value of a function at a given point by a given value. Decidability of equality in `ι` is needed to perform this updating operation. The theorem is universally quantified over all `X`, `ι`, `π`, `f`, `i` and `g` that satisfy the given conditions.
More concisely: If `f` is a continuous function from a topological space `X` to a dependent function type `(i : ι) → π i`, where each `π i` is a topological space, and `g` is a continuous function from `X` to some `π i`, then the function obtained by updating `f` with `g` using `Function.update` is also continuous.
|
ContinuousAt.fst
theorem ContinuousAt.fst :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : X → Y × Z} {x : X}, ContinuousAt f x → ContinuousAt (fun x => (f x).1) x
The theorem `ContinuousAt.fst` states that for all types `X`, `Y`, `Z`, provided `X`, `Y`, `Z` are topological spaces, for any function `f` from `X` to the Cartesian product of `Y` and `Z`, and for any point `x` in `X`, if the function `f` is continuous at the point `x`, then the function obtained by post-composing `f` with the first projection function (`Prod.fst`) is also continuous at the point `x`. In other words, if `f` is continuous at `x`, then the function that maps `x` to the `Y`-component of `f(x)` is also continuous at `x`.
More concisely: If `f: X → Y × Z` is a continuous function from a topological space `X` to the product of topological spaces `Y × Z`, then the composition of `f` with the first projection `Prod.fst` is also continuous at every point `x ∈ X` where `f` is continuous.
|
inducing_sigma
theorem inducing_sigma :
∀ {X : Type u} {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)]
[inst_1 : TopologicalSpace X] {f : Sigma σ → X},
Inducing f ↔
(∀ (i : ι), Inducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
The theorem `inducing_sigma` states that for any function `f` mapping from a sigma type (i.e., the disjoint union of an indexed family of topological spaces) to another topological space `X`, the function `f` is inducing if and only if two conditions are met: firstly, the function `f`, when restricted to each component of the sigma type, is inducing; secondly, for each component of the sigma type, there exists an open set `U` in `X` such that a point in the sigma type mapped by `f` is in `U` if and only if the first component of the point is equal to the index of the said component.
More concisely: A function from a sigma type to a topological space is inducing if and only if each restriction is inducing and there exists an open set in the target space mapping each component to itself under the function.
|
continuous_pi
theorem continuous_pi :
∀ {X : Type u} {ι : Type u_5} {π : ι → Type u_6} [inst : TopologicalSpace X] [T : (i : ι) → TopologicalSpace (π i)]
{f : X → (i : ι) → π i}, (∀ (i : ι), Continuous fun a => f a i) → Continuous f
This theorem, `continuous_pi`, establishes that for any type `X` with a topological space structure, any indexing type `ι`, and any type `π` indexed by `ι` and equipped with a family of topological space structures, a function `f` from `X` to `π` is continuous if and only if for each index `i` in `ι`, the function obtained by applying `f` and then projecting onto the `i`th component, is continuous. In other words, a function into a product space is continuous if and only if each of its component functions is continuous.
More concisely: A function from a topological space to a product of topological spaces is continuous if and only if each component function is continuous.
|
quotientMap_quot_mk
theorem quotientMap_quot_mk : ∀ {X : Type u} [inst : TopologicalSpace X] {r : X → X → Prop}, QuotientMap (Quot.mk r)
This theorem states that for any type 'X' equipped with a topological space structure, and for any equivalence relation 'r' on 'X', the function that sends each element of 'X' to its equivalence class under 'r' (denoted `Quot.mk r`) is a quotient map. Here, a quotient map is defined for a function between topological spaces that is surjective and for which a set in the codomain is open if and only if its preimage under the function is open in the domain.
More concisely: Given a topological space 'X' and an equivalence relation 'r' on 'X', the quotient function 'Quot.mk r' is a quotient map.
|
Continuous.snd'
theorem Continuous.snd' :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : Y → Z}, Continuous f → Continuous fun x => f x.2
The theorem `Continuous.snd'` states that for any three types `X`, `Y`, and `Z` that have a topological space structure and for any function `f` from `Y` to `Z` that is continuous, the function created by first applying the second part of a product (`Prod.snd`) and then applying `f` is also continuous. In mathematical terms, if we have a continuous function `f: Y -> Z`, then the function `g: X x Y -> Z` defined by `g(x, y) = f(y)` is also continuous.
More concisely: If `f: Y �ERCHANT Z` is a continuous function and `g: X × Y �ERCHANT Z` is defined by `g(x, y) := f(y)`, then `g` is also continuous.
|
continuous_inclusion
theorem continuous_inclusion :
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X} (h : s ⊆ t), Continuous (Set.inclusion h)
The theorem `continuous_inclusion` states that for any type `X` equipped with a topology, and any two subsets `s` and `t` of `X` such that `s` is a subset of `t`, the `inclusion` function from `s` to `t` is continuous. Here, the `inclusion` function is a function that maps any element from subset `s` to itself in the larger set `t`, under the assumption that `s` is included in `t`. This theorem is a fundamental result in topology that establishes the continuity of inclusion mappings between subsets of a topological space.
More concisely: If `X` is a topological space, and `s` is a subset of `t` in `X`, then the inclusion function from `s` to `t` is continuous.
|
Continuous.subtype_mk
theorem Continuous.subtype_mk :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {f : Y → X},
Continuous f → ∀ (hp : ∀ (x : Y), p (f x)), Continuous fun x => ⟨f x, ⋯⟩
This theorem states that for any two types `X` and `Y` with given topological space structures and a predicate `p` on `X`, if a function `f` from `Y` to `X` is continuous and for every element in `Y` the predicate `p` holds true for the image of that element under `f`, then the function that takes an element of `Y` and returns a subtype of `X` with the value being the image of the element under `f` and the property being the satisfaction of the predicate `p` is also continuous.
More concisely: If `f: Y → X` is a continuous function between topological spaces `X` and `Y` such that `p(x)` holds for all `x ∈ Y` implies `p(f(x))` holds for `p` a predicate on `X`, then the function `g : Y → Subtype X` defined by `g(y) = {x | p(x) and x = f(y)}` is continuous.
|
Mathlib.Topology.Constructions._auxLemma.10
theorem Mathlib.Topology.Constructions._auxLemma.10 :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : X → Y} {g : X → Z},
(Continuous fun x => (f x, g x)) = (Continuous f ∧ Continuous g)
This theorem, named `_auxLemma.10` in Mathlib's Topology Constructions, states that for any three types `X`, `Y`, and `Z` along with instances of these types being topological spaces, and given two functions `f : X → Y` and `g : X → Z`, the function that maps each element of `X` to a tuple with the result of applying `f` and `g` to that element is continuous if and only if both `f` and `g` are continuous. In mathematical terms, $\forall X, Y, Z, f : X \to Y, g : X \to Z$, the function $x \mapsto (f(x), g(x))$ is continuous iff both $f$ and $g$ are continuous.
More concisely: For any types X, Y, Z of topological spaces and continuous functions f : X -> Y and g : X -> Z, the function x => (f x, g x) is a continuous function from X to Y x Z.
|
DenseRange.quotient
theorem DenseRange.quotient :
∀ {X : Type u} {Y : Type v} [inst : Setoid X] [inst_1 : TopologicalSpace X] {f : Y → X},
DenseRange f → DenseRange (Quotient.mk' ∘ f)
This theorem states that if a function `f : Y → X` has a dense range in a topological space `X`, then the composition of `Quotient.mk'` and `f` also has a dense range. Here, `Quotient.mk'` is the canonical quotient mapping that takes an element in a set and maps it to its equivalence class in the quotient set defined by the setoid `X`. This theorem therefore relates the concepts of dense sets, quotient maps, and function composition in the context of topological spaces.
More concisely: If `f : Y → X` has a dense range in the topological space `X`, then the composition `Quotient.mk' ∘ f` also has a dense range in the quotient space `Quotient.mk' X`.
|
continuous_sInf_dom₂
theorem continuous_sInf_dom₂ :
∀ {X : Type u_5} {Y : Type u_6} {Z : Type u_7} {f : X → Y → Z} {tas : Set (TopologicalSpace X)}
{tbs : Set (TopologicalSpace Y)} {tX : TopologicalSpace X} {tY : TopologicalSpace Y} {tc : TopologicalSpace Z},
tX ∈ tas → tY ∈ tbs → (Continuous fun p => f p.1 p.2) → Continuous fun p => f p.1 p.2
This theorem, `continuous_sInf_dom₂`, asserts that for any three types `X`, `Y`, and `Z`, any binary function `f` from `X` and `Y` to `Z`, two sets of topological spaces `tas` and `tbs` over `X` and `Y` respectively, and the topological spaces `tX`, `tY`, and `tc` over `X`, `Y`, and `Z` respectively, if the topological space `tX` is an element of `tas`, the topological space `tY` is an element of `tbs`, and the function `(p => f p.1 p.2)` is continuous, then the function `(p => f p.1 p.2)` remains continuous. In simpler terms, it is a statement about the continuity of a binary function under certain conditions related to topological spaces.
More concisely: If `X`, `Y`, and `Z` are types, `f : X → Y → Z` is a continuous function, and `tas` and `tbs` are topological spaces over `X` and `Y` respectively, such that `tX ∈ tas` and `tY ∈ tbs`, then `(p => f p.1 p.2)` is a continuous function from the product topology on `X × Y` to `Z`.
|
continuous_single
theorem continuous_single :
∀ {ι : Type u_5} {π : ι → Type u_6} [T : (i : ι) → TopologicalSpace (π i)] [inst : (i : ι) → Zero (π i)]
[inst_1 : DecidableEq ι] (i : ι), Continuous fun x => Pi.single i x
The theorem `continuous_single` asserts that for every index type `ι`, every type function `π` mapping `ι` to another type, given a topological space over the type `π i` for each `i` in `ι` and a zero element of `π i` for each `i` in `ι`, and assuming that equality is decidable for `ι`, for any element `i` of `ι`, the function `Pi.single i` is continuous. In other words, the function which assigns to each `x` the function `Pi.single i x` (which maps `i` to `x` and every other element of `ι` to `0`) is a continuous function.
More concisely: Given a topological space and a zero element for each index of an index type, the function assigning to each index its evaluation at a point is continuous if equality is decidable for the index type.
|
Embedding.codRestrict
theorem Embedding.codRestrict :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {e : X → Y},
Embedding e → ∀ (s : Set Y) (hs : ∀ (x : X), e x ∈ s), Embedding (Set.codRestrict e s hs)
The theorem `Embedding.codRestrict` states that for any two types `X` and `Y`, with each having a topological space structure, and given a function `e` from `X` to `Y` that is an embedding, for any set `s` of `Y` such that every image of `e` is in `s`, the function obtained by restricting the codomain of `e` to `s` is also an embedding. In other words, if `e` is an embedding, then the function that sends each element `x` in `X` to the element in `s` corresponding to `e(x)` (with a proof that `e(x)` is indeed in `s`), is also an embedding.
More concisely: If `e: X → Y` is an embedding of topological spaces `X` and `Y`, then the restriction of `e` to the image of `e` is also an embedding from `X` to the subspace of `Y` consisting of the images of points in `X`.
|
IsOpen.openEmbedding_subtype_val
theorem IsOpen.openEmbedding_subtype_val :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → OpenEmbedding Subtype.val
This theorem states that for any set `s` of a type `X` equipped with a topological space structure, if `s` is open in this topology, then the function `Subtype.val` is an open embedding. In other words, the mapping that takes each element of the subtype defined by `s` (which consists of elements `x` of `X` for which the predicate `p(x)` holds) to the underlying base type `X` preserves the topology on `s` and embeds `s` as an open set in `X`.
More concisely: For any subspace `s` of a topological space `(X,τ)` with the property that `s` is open in `(X,τ)`, the subtype embedding `Subtype.val : s ↪ X` is an open map.
|
isOpen_set_pi
theorem isOpen_set_pi :
∀ {ι : Type u_5} {π : ι → Type u_6} [T : (i : ι) → TopologicalSpace (π i)] {i : Set ι} {s : (a : ι) → Set (π a)},
i.Finite → (∀ a ∈ i, IsOpen (s a)) → IsOpen (i.pi s)
The theorem `isOpen_set_pi` states that for any type `ι`, any function `π` mapping `ι` to a type, a topological space on each type `π i`, a set `i` of type `ι`, and a family of sets `s` indexed by `ι` and mapping to each type `π a`, if the set `i` is finite and each set `s a` is open for all `a` in `i`, then the set of all dependent functions `f` such that `f a` belongs to `s a` for all `a` in `i`, denoted as `Set.pi i s`, is also an open set. In other words, the cartesian product of a finite number of open sets is an open set in the product topology.
More concisely: For a finite index type `ι`, a function `π : ι → Type`, a topological space on each `π i`, a set `i` of type `ι`, and a family `s : ∀ a, π a → Set`, if each `s a` is an open set in the subspace topology on `π a`, then `Set.pi i s` is an open set in the product topology on `Π a, s a`.
|
continuous_fst
theorem continuous_fst :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Continuous Prod.fst := by
sorry
This theorem, `continuous_fst`, states that for any two types `X` and `Y` equipped with topological spaces (denoted by `inst : TopologicalSpace X` and `inst_1 : TopologicalSpace Y`), the function `Prod.fst`, which projects an ordered pair to its first component, is continuous. In other words, if we have a pair from the Cartesian product of `X` and `Y`, taking the first component of the pair and mapping it back to `X` preserves topological properties. In mathematical terms, if `p : X × Y`, then the function `p ↦ p.1` is continuous.
More concisely: The function `Prod.fst` from a Cartesian product `X × Y` equipped with product topology to `X` is continuous.
|
continuous_sigma
theorem continuous_sigma :
∀ {X : Type u} {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)]
[inst_1 : TopologicalSpace X] {f : Sigma σ → X}, (∀ (i : ι), Continuous fun a => f ⟨i, a⟩) → Continuous f
This theorem states that a function `f` from a sum type `Sigma σ` to a type `X` is continuous if its restriction to each component type (or summand) `σ i` is continuous. Here, `X` and each `σ i` are equipped with topological space structures. The sum type `Sigma σ` is a dependent type, which can be thought of as a type of "tagged" or "labeled" elements, with each label coming from the type `ι` and each element being from the corresponding type `σ i`.
More concisely: A function from a dependent sum type to a topological space is continuous if and only if its restriction to each summand is continuous.
|
embedding_subtype_val
theorem embedding_subtype_val : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop}, Embedding Subtype.val := by
sorry
The theorem `embedding_subtype_val` states that for any type `X` with a topology (denoted by `TopologicalSpace X`), and for any predicate `p` on `X`, the function `Subtype.val` (which extracts the underlying element from a subtype defined by `p`) is an embedding. In other words, this function preserves the topological properties of the elements from the subtype to the original type `X`.
More concisely: The function `Subtype.val` from a subtype of a topological space `X` defined by a predicate `p` is a topological embedding.
|
Continuous.fst
theorem Continuous.fst :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : X → Y × Z}, Continuous f → Continuous fun x => (f x).1
This theorem states that for any three types `X`, `Y`, `Z` that are equipped with topological structures, if we have a continuous function `f` from `X` to the cartesian product of `Y` and `Z` (`Y × Z`), then the function obtained by composing `f` with the `Prod.fst` function (which extracts the first component of a pair) is also continuous. In mathematical terms, the theorem says that if `f : X → Y × Z` is a continuous function, then the function `x ↦ (f(x)).1` is continuous.
More concisely: If `f : X → Y × Z` is a continuous function, then the function `x ↦ (f(x)).1` extracting the first component from the product is also continuous.
|
IsOpen.isOpenMap_subtype_val
theorem IsOpen.isOpenMap_subtype_val :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → IsOpenMap Subtype.val
The theorem `IsOpen.isOpenMap_subtype_val` states that for any type `X` with a topological space structure and any set `s` in `X`, if `s` is open in the topological space of `X`, then the projection map (`Subtype.val`), which sends each element of the subtype `{x // x ∈ s}` to its underlying element in `X`, is an open map. In other words, this theorem guarantees that the image of any open set under the projection map is also an open set in the topological space of `X`.
More concisely: The projection map of an open subtype is open.
|
continuous_update
theorem continuous_update :
∀ {ι : Type u_5} {π : ι → Type u_6} [T : (i : ι) → TopologicalSpace (π i)] [inst : DecidableEq ι] (i : ι),
Continuous fun f => Function.update f.1 i f.2
The theorem `continuous_update` states that the operation `Function.update f i x`, which replaces the value of function `f` at point `i` by value `x`, is continuous with respect to `(f, x)`. Here, `ι` is a type, `π` is a type dependent on `ι`, and each `π i` is equipped with a topological space structure. This theorem holds for all `i` of type `ι` and the equality of `ι` is decidable.
More concisely: For all types `ι` with decidable equality and each `π` type dependent on `ι` equipped with a topology, the function update operation `Function.update f i x : π -> π` is continuous with respect to its arguments `(f : π i, x : π)`.
|
isOpenMap_inl
theorem isOpenMap_inl :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsOpenMap Sum.inl
The theorem `isOpenMap_inl` states that for any types `X` and `Y`, given that `X` and `Y` both have topological space structures, the left injection function `Sum.inl` from `X` into the sum type `X + Y` (written as `Sum X Y` in Lean), is an open map. In other words, for any open set in `X`, its image under the `Sum.inl` function is an open set in the sum space `X + Y`.
More concisely: The left injection map from a topological space `X` into the sum `X + Y` preserves open sets.
|
Dense.prod
theorem Dense.prod :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
Dense s → Dense t → Dense (s ×ˢ t)
This theorem states that the product of two dense sets is a dense set. In other words, if we have two topological spaces `X` and `Y`, and `s` is a dense set in `X` and `t` is a dense set in `Y`, then the product set `s ×ˢ t` is a dense set in the product topological space `X × Y`. In terms of topology, a set is dense if every point in the space is either in the set or is a limit point of the set, meaning that every open ball contains a point from the set. Therefore, this theorem ensures that the concept of denseness is preserved under the operation of forming the product of two sets.
More concisely: If two sets `s` in topological space `X` and `t` in `Y` are dense, then their product `s ×ˢ t` is dense in the product topological space `X × Y`.
|
map_fst_nhds
theorem map_fst_nhds :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X × Y),
Filter.map Prod.fst (nhds x) = nhds x.1
This theorem, `map_fst_nhds`, states that for any types `X` and `Y` with topological space structures, and for any point `x` in the product space `X × Y`, the map of the neighborhood filter at `x` under the first projection `Prod.fst` is the neighborhood filter at `x.1` (i.e., `Prod.fst x`). In other words, if we take the filter of all neighborhoods of a point in the product space `X × Y`, and then project each of these neighborhoods onto the `X` space, we get the neighborhood filter of the projection of the point in `X`.
More concisely: For any topological spaces X and Y and point (x, y) in X × Y, the neighborhood filter of x in X under the first projection is equal to the neighborhood filter of y in X × Y under the first projection.
|
Continuous.Prod.mk_left
theorem Continuous.Prod.mk_left :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (y : Y),
Continuous fun x => (x, y)
This theorem, `Continuous.Prod.mk_left`, states that for any two types `X` and `Y` with `TopologicalSpace` instances, and any fixed element `y` of type `Y`, the function that takes an element `x` of type `X` and pairs it with the fixed `y` to form a pair `(x, y)` is a continuous function. This is stated in the context of topology, where continuity has a specific mathematical meaning related to the preservation of nearness.
More concisely: For any topological spaces X and Y, and any fixed y in Y, the function x ═> (x, y) from X to X xico Y is continuous.
|
inducing_iInf_to_pi
theorem inducing_iInf_to_pi :
∀ {ι : Type u_5} {π : ι → Type u_6} [T : (i : ι) → TopologicalSpace (π i)] {X : Type u_8} (f : (i : ι) → X → π i),
Inducing fun x i => f i x
This theorem states that if we have a family of topological spaces `π i`, indexed by `i : ι`, and a type `X` that is associated with a family of maps `f i : X → π i` for every `i : ι`, creating an induced map `g : X → Π i, π i`, then the infimum of the topologies on `X` induced by the `f i` as `i : ι` varies, is simply the topology on `X` induced by `g`. Here, `Π i, π i` is equipped with the usual product topology.
More concisely: The theorem asserts that the topology on a type `X` induced by a family of maps `f i : X → π i` is equal to the product topology on `X` induced by the family of topologies `{π i : Top | i : ι}`.
|
continuous_swap
theorem continuous_swap :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Continuous Prod.swap := by
sorry
The theorem `continuous_swap` states that for any given types `X` and `Y`, with `X` and `Y` being topological spaces, the function `Prod.swap`, which swaps the factors of a product, is a continuous function. In other words, swapping the elements of ordered pairs doesn't disrupt the topology or connectedness of the space.
More concisely: The `Prod.swap` function on the product of topological spaces `X` and `Y` is a continuous function.
|
closure_prod_eq
theorem closure_prod_eq :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
closure (s ×ˢ t) = closure s ×ˢ closure t
The theorem `closure_prod_eq` states that for all types `X` and `Y` with topological space structures, and for any two sets `s` of type `X` and `t` of type `Y`, the closure of the Cartesian product of `s` and `t` is equal to the Cartesian product of the closures of `s` and `t`. In mathematical notation, this is saying that for any two sets `s` and `t` in topological spaces `X` and `Y` respectively, `cl(s x t) = cl(s) x cl(t)`, where `cl` denotes the topological closure operation and `x` denotes the Cartesian product of two sets.
More concisely: For any topological spaces X and Y, and sets s in X and t in Y, the closure of their Cartesian product s × t is equal to the Cartesian product of the closures of s and t, i.e., cl(s × t) = cl(s) × cl(t).
|
map_nhds_subtype_val
theorem map_nhds_subtype_val :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} (x : ↑s),
Filter.map Subtype.val (nhds x) = nhdsWithin (↑x) s
This theorem states that for any topological space `X` and a subset `s` of `X`, the image under the function `Subtype.val` (which extracts the underlying element from a subtype) of the neighborhood filter of an element `x` of the subtype of `s` is equal to the neighborhood filter of `x` within the set `s`. In simpler terms, it's saying that the neighborhoods of a point in the subtype correspond to the neighborhoods of the point in the original space restricted to the subset.
More concisely: For any topological space X and a subset s of X, the neighborhood filter of an element x in the subtype of s is equal to the restriction to s of the neighborhood filter of x in X.
|
prod_mem_nhds
theorem prod_mem_nhds :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y}
{x : X} {y : Y}, s ∈ nhds x → t ∈ nhds y → s ×ˢ t ∈ nhds (x, y)
This theorem states that for any two topological spaces `X` and `Y`, and any sets `s` and `t` where `s` is a neighborhood of a point `x` in `X` and `t` is a neighborhood of a point `y` in `Y`, the Cartesian product of `s` and `t` is a neighborhood of the point `(x, y)` in the product space `X × Y`. In other words, if `s` is near `x` and `t` is near `y`, then `s × t` is near `(x, y)`. This is a property that intuitively makes sense in the context of topological spaces, and forms a fundamental part of the definition of a product topology.
More concisely: Given topological spaces X and Y, and neighborhoods s of a point x in X and t of a point y in Y, the product neighborhood s × t in X × Y is a neighborhood of (x, y).
|
tendsto_subtype_rng
theorem tendsto_subtype_rng :
∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type u_5} {p : X → Prop} {l : Filter Y} {f : Y → Subtype p}
{x : Subtype p}, Filter.Tendsto f l (nhds x) ↔ Filter.Tendsto (fun x => ↑(f x)) l (nhds ↑x)
The theorem `tendsto_subtype_rng` states that for any topological space `X`, any type `Y`, any property `p` of `X`, any filter `l` on `Y`, any function `f` from `Y` to `Subtype p` and any element `x` of `Subtype p`, the function `f` tends to the neighborhood filter of `x` if and only if the function which applies `f` and then takes the underlying element of `Subtype p` tends to the neighborhood filter of the underlying element of `x`. In other words, it asserts that the limit of a function into a subtype is equivalent to the limit of the same function composed with the subtype's inclusion function, into the original type.
More concisely: For any topological space X, type Y, property p of X, filter l on Y, function f from Y to Subtype p over X, and element x of Subtype p, the function f tends to the neighborhood filter of x if and only if the composition of f with the inclusion function of Subtype p into X tends to the neighborhood filter of x's underlying element in X.
|
openEmbedding_inl
theorem openEmbedding_inl :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], OpenEmbedding Sum.inl := by
sorry
This theorem states that for any two types `X` and `Y` each equipped with a topology (i.e., `X` and `Y` are topological spaces), the injection function `Sum.inl` from `X` into the sum type `X + Y` is an open embedding. In the context of topology, an open embedding is a function which is both an embedding and the image of any open set is open. In simpler terms, it preserves the topological structure of the original space, and specifically the openness of sets.
More concisely: The injection function `Sum.inl` from a topological space `X` into the sum type `X + Y` is a topological embedding.
|
continuous_snd
theorem continuous_snd :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Continuous Prod.snd := by
sorry
This theorem, `continuous_snd`, states that for all types `X` and `Y` where `X` and `Y` are equipped with a topological space structure (denoted by `inst` and `inst_1` respectively), the second projection function `Prod.snd` is continuous. In mathematical terms, this means that if we have a product space `X × Y`, the function that maps each pair to the second element of the pair is a continuous function.
More concisely: The second projection function of a product of topological spaces is continuous.
|
isOpenMap_fst
theorem isOpenMap_fst :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsOpenMap Prod.fst := by
sorry
The theorem `isOpenMap_fst` states that for any pair of topological spaces `X` and `Y`, the first projection function `Prod.fst` is an open map. This means that if we take an open set in the product space `X × Y`, the image of this set under `Prod.fst`, which is a subset of `X`, is also an open set in `X`. In simpler terms, applying the first projection to an open set in the product space will result in an open set in the first topological space.
More concisely: For any topological spaces X and Y, the first projection function Prod.fst from X × Y to X is an open map.
|
Continuous.snd
theorem Continuous.snd :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : X → Y × Z}, Continuous f → Continuous fun x => (f x).2
This theorem states that for any three types `X`, `Y`, and `Z`, given that `X`, `Y`, and `Z` are topological spaces, and there is a continuous function `f` from `X` to the product space `Y × Z`, the function obtained by post-composing `f` with `Prod.snd` (which extracts the second component of the product) is also continuous. In other words, if `f` is a continuous function that produces pairs of elements, the operation of taking the second element of the pair produced by `f` is also a continuous function.
More concisely: Given three topological spaces X, Y, and Z, and a continuous function f : X → Y × Z, the function Proj.snd ∘ f : X → Z is continuous.
|
IsClosed.setOf_mapsTo
theorem IsClosed.setOf_mapsTo :
∀ {X : Type u} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Z] {α : Type u_5}
{f : X → α → Z} {s : Set α} {t : Set Z},
IsClosed t → (∀ a ∈ s, Continuous fun x => f x a) → IsClosed {x | Set.MapsTo (f x) s t}
This theorem states that if a function `f` mapping from `X` to `Z` is continuous in its first argument for all elements in a set `s` of type `α`, and if `t`, a set in topological space `Z`, is a closed set, then the set of all those elements of `X` for which `f` maps `s` into `t` is also a closed set in its own topological space.
In other words, if you have a function `f` that takes an element of type `X` and an element of type `α` and returns an element of type `Z`, then if `f` is continuous with respect to its first argument for all elements in a certain set `s`, and if `t` is a closed set of `Z`, then the set of all `x` in `X` such that `f x` maps all elements of `s` into `t` is a closed set in the topological space of `X`.
More concisely: If a continuous function from X to Z maps a closed set in α to a closed set in Z for all elements in a subset s of α, then the preimage of that closed set in Z under the function is a closed set in X.
|
nhdsWithin_prod_eq
theorem nhdsWithin_prod_eq :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X) (y : Y) (s : Set X)
(t : Set Y), nhdsWithin (x, y) (s ×ˢ t) = nhdsWithin x s ×ˢ nhdsWithin y t
This theorem states that for any two types `X` and `Y` with respective topological spaces, and any elements `x` from `X` and `y` from `Y`, and any sets `s` of `X` and `t` of `Y`, the neighborhood within filter of the pair `(x, y)` in the product set `s ×ˢ t` is equal to the product of the neighborhood within filter of `x` in `s` and the neighborhood within filter of `y` in `t`. In more mathematical terms, it states that the operation of taking neighborhood within filters distributes over Cartesian product of sets in topological spaces.
More concisely: The neighborhood filters of elements in topological spaces distribute over the Cartesian product, that is, the neighborhood filter of a pair in the product of two sets is equal to the product of the neighborhood filters of the elements in the pair.
|
ContinuousAt.fst''
theorem ContinuousAt.fst'' :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : X → Z} {x : X × Y}, ContinuousAt f x.1 → ContinuousAt (fun x => f x.1) x
The theorem `ContinuousAt.fst''` states that for any types `X`, `Y`, and `Z` equipped with topological spaces, and given a function `f` from `X` to `Z` and a point `x` in the product space `X × Y`, if `f` is continuous at the first component of `x`, then the function obtained by precomposing `f` with the projection onto the first component (`Prod.fst`) is also continuous at `x`. In other words, if `f` doesn't cause "jumps" when inputs approach a point in `X`, then neither does the function that takes a pair in `X × Y`, projects it to `X`, and then applies `f`.
More concisely: If `f : X → Z` is continuous at `x ∈ X × Y` and `Prod.fst : X × Y → X` is the projection onto the first component, then the composition `f ∘ Prod.fst` is continuous at `x`.
|
continuous_quot_lift
theorem continuous_quot_lift :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {r : X → X → Prop} {f : X → Y}
(hr : ∀ (a b : X), r a b → f a = f b), Continuous f → Continuous (Quot.lift f hr)
This theorem states that for any types `X` and `Y`, where `X` and `Y` are endowed with topological structures, if we have a relation `r` on `X` and a function `f` from `X` to `Y` such that `f` respects the relation `r` (i.e., `f` gives the same output for any two elements of `X` that are related by `r`), then if `f` is continuous, the 'lift' of `f` to the quotient of `X` by `r` (represented by `Quot.lift f hr`) is also continuous. In terms of mathematical language, if $X$ and $Y$ are topological spaces, $r$ is an equivalence relation on $X$, and $f: X \rightarrow Y$ is a continuous function that is constant on $r$-equivalence classes, then the induced function on the quotient space $X/r$ is also continuous.
More concisely: If `X` and `Y` are topological spaces, `r` is an equivalence relation on `X`, `f: X → Y` is a continuous function that is constant on `r`-equivalence classes, then the induced function `Quot.lift f hr` on the quotient space `X/r` is continuous.
|
DiscreteTopology.of_subset
theorem DiscreteTopology.of_subset :
∀ {X : Type u_5} [inst : TopologicalSpace X] {s t : Set X}, DiscreteTopology ↑s → t ⊆ s → DiscreteTopology ↑t := by
sorry
This theorem states that given `s` and `t` as two subsets of a topological space `X`, if `t` is a subset of `s` and the topology induced on `s` by `X` is discrete, then the topology induced on `t` is also discrete. In other words, the discreteness of the topology induced on a set is preserved under taking subsets.
More concisely: If a subset `t` of a topological space `X` is discrete when considered as a subspace of `X` with the induced topology, then it is also a discrete topology as a subspace of `X`.
|
isOpenMap_snd
theorem isOpenMap_snd :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsOpenMap Prod.snd := by
sorry
The theorem `isOpenMap_snd` states that for any two topological spaces `X` and `Y`, the second projection function `Prod.snd`, which takes a pair in the product space `X × Y` and returns its second component in `Y`, is an open map. In other words, if a set in the product space `X × Y` is open, then its image under the second projection (consisting of the 'Y'-components of the pairs) is also an open set in `Y`.
More concisely: The second projection of a product space is an open map, that is, the image of an open set under the second projection is an open set in the second factor space.
|
isOpen_prod_iff'
theorem isOpen_prod_iff' :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
The theorem `isOpen_prod_iff'` states that for any two types `X` and `Y` equipped with topological spaces, and any sets `s` of `X` and `t` of `Y`, the product set `s ×ˢ t` is open in the product space if and only if either both sets `s` and `t` are open, or one of the sets `s` and `t` is empty. This theorem provides a condition for the openness of a product set in a product space.
More concisely: A product set in a product space is open if and only if both factors are open or one of them is empty.
|
IsClosed.closedEmbedding_subtype_val
theorem IsClosed.closedEmbedding_subtype_val :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → ClosedEmbedding Subtype.val
This theorem states that for any type `X` with a topological space structure, and any set `s` of `X`, if `s` is a closed set (i.e., `IsClosed s`), then the function `Subtype.val` forms a closed embedding. The `Subtype.val` function takes a subtype (elements of the base type `X` that satisfy a certain predicate) and returns the underlying element in the base type. A closed embedding is a function that is both a homeomorphism onto its image (i.e., it preserves the topological structure) and a closed map (i.e., it sends closed sets to closed sets).
More concisely: If `X` is a topological space and `s` is a closed subset of `X`, then the inclusion function from `s` to its image under `Subtype.val` is a closed embedding.
|
Dense.quotient
theorem Dense.quotient :
∀ {X : Type u} [inst : Setoid X] [inst_1 : TopologicalSpace X] {s : Set X}, Dense s → Dense (Quotient.mk' '' s)
This theorem states that the image of a dense set under the function `Quotient.mk'` is also a dense set. Here, a set is considered dense in a topological space if every point belongs to its closure. Therefore, if we have a dense set in a topological space with an underlying Setoid structure, and we apply the quotient map `Quotient.mk'` to all elements of this set, the resulting set maintains the property of being dense in its respective topological space.
More concisely: If a set is dense in a topological space with an underlying Setoid structure, then the image of that set under the quotient map `Quotient.mk'` is also a dense set in the same topological space.
|
openEmbedding_inr
theorem openEmbedding_inr :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], OpenEmbedding Sum.inr := by
sorry
This theorem states that for any two types `X` and `Y` with respective topological spaces, `Sum.inr` (the function that takes an item of type `Y` and returns an item of the sum type `X + Y`) is an open embedding. An open embedding is a function between topological spaces that is injective (i.e., distinct inputs map to distinct outputs), continuous (i.e., the preimage of an open set is open), and its image is an open subset in the codomain. This means that `Sum.inr` has these properties when considered as a function from `Y` to `X + Y` with the given topologies.
More concisely: The function `Sum.inr`: `Y → X + Y` is an open embedding between the topological spaces of types `Y` and `X + Y`.
|
ContinuousAt.fst'
theorem ContinuousAt.fst' :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : X → Z} {x : X} {y : Y},
ContinuousAt f x → ContinuousAt (fun x => f x.1) (x, y)
This theorem states that if a function `f` from a topological space `X` to a topological space `Z` is continuous at a point `x` in `X`, then the function obtained by precomposing `f` with the first projection `Prod.fst` (which sends a pair `(x, y)` to `x`) is continuous at any point `(x, y)` in the product space `X × Y`. In other words, if `f` is continuous at a point, then it remains continuous when considered on the product of its domain with any other topological space, evaluated at points that have the original point as their first component.
More concisely: If a function `f: X → Z` is continuous at a point `x ∈ X`, then the composed function `f ∘ Prod.fst: X × Y → Z` is continuous at any `(x, y) ∈ X × Y`.
|
CofiniteTopology.nhds_eq
theorem CofiniteTopology.nhds_eq : ∀ {X : Type u} (x : CofiniteTopology X), nhds x = pure x ⊔ Filter.cofinite := by
sorry
This theorem states that for any type `X` and an element `x` of type `X` equipped with the cofinite topology, the neighborhood filter at `x` is equal to the join of the pure filter of `x` and the cofinite filter. In other words, a set is a neighborhood of `x` in the cofinite topology if and only if it contains `x` and its complement is finite.
More concisely: In the cofinite topology on any type `X` and element `x` of `X`, the neighborhood filter of `x` equals the join of the pure filter of `x` and the cofinite filter. (Equivalently, a set is a neighborhood of `x` if and only if it contains `x` and has finite complement.)
|
Continuous.subtype_map
theorem Continuous.subtype_map :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {f : X → Y},
Continuous f → ∀ {q : Y → Prop} (hpq : ∀ (x : X), p x → q (f x)), Continuous (Subtype.map f hpq)
The theorem `Continuous.subtype_map` states that for any two types `X` and `Y` equipped with topological spaces, and a property `p` on `X`, if a function `f : X → Y` is continuous, then for any property `q` on `Y` such that `q` holds for `f(x)` whenever `p` holds for `x`, the restricted function `Subtype.map f hpq`, which maps each subtype `x` of `X` satisfying `p` to subtype `f(x)` of `Y` satisfying `q`, is also continuous. This means the continuity of a function is preserved when it is restricted to subsets of its domain and codomain defined by properties `p` and `q` respectively.
More concisely: If `f : X → Y` is a continuous function between topological spaces `X` and `Y`, and `p : Prop` and `q : Prop` are properties such that `q` holds for `f(x)` whenever `p` holds for `x`, then the function `Subtype.map f (Prop p) : Subtype X p → Subtype Y (Prop.and p (image p _ f))` is continuous.
|
quotientMap_quotient_mk'
theorem quotientMap_quotient_mk' :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Setoid X}, QuotientMap Quotient.mk'
This theorem states that for any type `X` equipped with a topological space structure and any setoid `s` over `X`, the canonical quotient map `Quotient.mk'` (which maps each element of `X` to its equivalence class in the quotient set `Quotient s`) is a quotient map. In other words, the function `Quotient.mk'` is surjective and for any set `s` in the resulting quotient structure, `s` is open if and only if its pre-image under `Quotient.mk'` is an open set in `X`.
More concisely: Given a topological space `(X, top)` and a setoid `s` over `X`, the canonical quotient map `Quotient.mk' : X → Quotient s` is a quotient map, that is, it is surjective and preserves open sets.
|
ContinuousAt.codRestrict
theorem ContinuousAt.codRestrict :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {t : Set Y}
(h1 : ∀ (x : X), f x ∈ t) {x : X}, ContinuousAt f x → ContinuousAt (Set.codRestrict f t h1) x
The theorem `ContinuousAt.codRestrict` states that for any topological spaces `X` and `Y`, given a function `f` from `X` to `Y` and a set `t` of `Y` such that every output of `f` belongs to `t`, if `f` is continuous at a point `x` in `X`, then the function `f` restricted to the set `t` (using `Set.codRestrict`) is also continuous at `x`. Essentially, this theorem guarantees that restricting the codomain of a continuous function to a set that includes all its outputs does not affect the continuity of the function at a given point.
More concisely: If `f: X → Y` is continuous at `x ∈ X` and `t ⊆ Y` contains all images of `f`, then `f|t: X → t` is continuous at `x`.
|
map_fst_nhdsWithin
theorem map_fst_nhdsWithin :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X × Y),
Filter.map Prod.fst (nhdsWithin x (Prod.snd ⁻¹' {x.2})) = nhds x.1
The theorem `map_fst_nhdsWithin` states that for any given point `x` of type `X × Y` where `X` and `Y` are topological spaces, the forward map of a filter `Prod.fst` applied to the "neighborhood within" filter at `x` in the preimage of `{x.2}` under `Prod.snd` is equal to the neighborhood filter at `x.1`. In simpler terms, it means that the first projection (`Prod.fst`) maps the neighborhood of a point `x` within the section defined by the second projection (`Prod.snd`) of `x.2` to the neighborhood of `x.1`.
More concisely: For any point `x` in a product topological space `X × Y`, the filter of neighborhoods of `x.1` under `Prod.fst` is equal to the preimage under `Prod.snd` of the neighborhood filter of `x.2` in the subspace `Y`.
|
Mathlib.Topology.Constructions._auxLemma.15
theorem Mathlib.Topology.Constructions._auxLemma.15 : ∀ {a b c : Prop}, (a ∧ b ∧ c) = (b ∧ a ∧ c)
This theorem states that for any three propositions `a`, `b`, and `c`, the conjunction of `a`, `b`, and `c` is the same as the conjunction of `b`, `a`, and `c`. In other words, the order in which the propositions are conjoined does not matter. This is analogous to the commutative property in basic arithmetic where the order of the numbers in the operation does not change the result (e.g., `a + b = b + a`).
More concisely: The theorem asserts the commutativity of proposition conjunction: `a ∧ b = b ∧ a`.
|
isOpenMap_sigmaMk
theorem isOpenMap_sigmaMk :
∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {i : ι}, IsOpenMap (Sigma.mk i) := by
sorry
The theorem `isOpenMap_sigmaMk` states that for every index set `ι` and a corresponding function `σ` that maps each index to a topological space, for any given index `i` from `ι`, the function `Sigma.mk i` is an open map. Here, `Sigma.mk i` is a function that takes an element from the topological space associated with the given index `i` and produces a sigma type (or dependent pair) consisting of the index `i` and the element from the topological space. An open map, in this context, means that the image of any open set under the function `Sigma.mk i` is also an open set.
More concisely: For any index set `ι` and a function `σ : ι → Top`, the function `Σ.mk : ∀ i : ι, σ i → Σ i × σ i` is an open map.
|
Pi.continuous_restrict
theorem Pi.continuous_restrict :
∀ {ι : Type u_5} {π : ι → Type u_6} [T : (i : ι) → TopologicalSpace (π i)] (S : Set ι), Continuous S.restrict := by
sorry
This theorem, named `Pi.continuous_restrict`, states that for all index types `ι` and all type families `π` indexed by `ι`, where each type in the family `π` is equipped with a topological space structure, and for any given set `S` of type `ι`, the function `Set.restrict S` is continuous. In other words, the restriction of a function to a subset `S` of its domain is always a continuous function, provided that the type of elements in `S` is `ι` and each type in the family `π` indexed by `ι` has a topology.
More concisely: For any index type `ι` and type family `π` indexed by `ι`, where each `π i` has a topology, the restriction function `Set.restrict S : π i -> Set S` is continuous for every set `S` of type `ι`.
|
continuousAt_snd
theorem continuousAt_snd :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X × Y},
ContinuousAt Prod.snd p
This theorem states that for any pair of types `X` and `Y`, both equipped with a topological space structure, and for any pair `p` of elements from `X` and `Y`, the second projection function `Prod.snd` is continuous at `p`.
In other words, as a point in the product space `X × Y` approaches `p`, the value of the function `Prod.snd` at that point (which is the corresponding `Y` component) tends to the `Y` component of `p`. This is the definition of continuity at a point in the context of topological spaces.
More concisely: For any topological spaces `X` and `Y` and any point `p` in their product `X × Y`, the second projection function `Prod.snd` is continuous at `p`.
|
exists_nhds_square
theorem exists_nhds_square :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set (X × X)} {x : X},
s ∈ nhds (x, x) → ∃ U, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s
This theorem states that for any topological space `X`, a set `s` of ordered pairs in `X`, and an element `x` of `X`, if `s` is a neighborhood of the pair `(x, x)`, then there exists an open set `U` such that `x` is an element of `U` and the Cartesian product of `U` with itself is a subset of `s`. In other words, around every point in a topological space, we can find a "square" open neighborhood that fits within any given neighborhood of that point.
More concisely: For any topological space `X` and point `x` in `X`, if `s` is a neighborhood of `(x, x)` in `X × X`, then there exists an open set `U` in `X` containing `x` such that `U × U ⊆ s`.
|
map_mem_closure₂
theorem map_mem_closure₂ :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : X → Y → Z} {x : X} {y : Y} {s : Set X} {t : Set Y} {u : Set Z},
Continuous (Function.uncurry f) →
x ∈ closure s → y ∈ closure t → (∀ a ∈ s, ∀ b ∈ t, f a b ∈ u) → f x y ∈ closure u
The theorem `map_mem_closure₂` states that for any three topological spaces `X`, `Y`, and `Z`, and for any function `f` from `X` to `Y` to `Z`, if the function `f` is continuous when uncurried, then for any points `x` in the closure of set `s` and `y` in the closure of set `t`, and for all elements `a` in set `s` and `b` in set `t` such that `f a b` belongs to set `u`, it follows that the function `f` applied to `x` and `y` belongs to the closure of set `u`.
In other words, this theorem is a result about continuous functions and closures in topological spaces. It specifically deals with the case where the function is uncurried - i.e., it takes a pair of inputs instead of a single one. It asserts that the image under such a function of a point from the closure of a product of two sets is contained in the closure of the image of that product set under the function.
More concisely: If functions `f : X × X → Z` are uncurried continuous, then for any sets `s ⊆ X` and `t ⊆ Y` such that `f(s × t) ⊆ u`, and for all `a ∈ s`, `b ∈ t`, and `f(a, b) ∈ u`, it follows that `f(cl(a), cl(b)) ∈ cl(u)`, where `cl` denotes the closure operator.
|
ContinuousAt.snd
theorem ContinuousAt.snd :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : X → Y × Z} {x : X}, ContinuousAt f x → ContinuousAt (fun x => (f x).2) x
This theorem states that if a function `f` from a type `X` to a product type `Y × Z` is continuous at a point `x` in the domain `X`, then the function that sends `x` to the second component of `f(x)` is also continuous at `x`. Here, `X`, `Y`, and `Z` are types equipped with topological structures, and continuity is defined in the sense of topological spaces. In other words, if the function `f` maps values close to `x` to values close to `f(x)`, the same holds true when we only consider the second component of `f(x)`.
More concisely: If `f : X → Y × Z` is continuous at `x ∈ X` then the projection function `π₂ : Y × Z → Z` applied to `f(x)` is continuous at `x`.
|
prod_induced_induced
theorem prod_induced_induced :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} {W : Type u_2} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace W]
(f : X → Y) (g : Z → W),
instTopologicalSpaceProd = TopologicalSpace.induced (fun p => (f p.1, g p.2)) instTopologicalSpaceProd
The theorem `prod_induced_induced` states that for any types `X`, `Y`, `Z`, `W`, given two functions `f : X → Y` and `g : Z → W` and topologies on `Y` and `W`, the topology on the product space `X × Z` induced by the topologies on `X` and `Z` is actually equivalent to the topology induced by the function mapping `p` in `X × Z` to `(f(p.1), g(p.2))` in `Y × W` under the product topology on `Y × W`. This means that the coarsest topology that makes both `f` and `g` continuous is the same as the product of the topologies induced by `f` and `g` respectively.
More concisely: The topology on the product space X × Z induced by the topologies on X and Z is equivalent to the topology on the product space Y × W induced by the function mapping (x, z) to (f(x), g(z)) under the product topology, where f : X → Y and g : Z → W.
|
continuous_quotient_mk'
theorem continuous_quotient_mk' : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Setoid X}, Continuous Quotient.mk'
This theorem states that for any type `X` equipped with a topological space structure, and any equivalence relation `s` on `X` (which forms a `Setoid X`), the canonical quotient map `Quotient.mk'` (which maps an element of `X` to its equivalence class in the quotient space `Quotient s`) is a continuous function. In other words, the image under `Quotient.mk'` of an open set in `X` is an open set in the quotient space.
More concisely: The quotient map of a continuous function and an equivalence relation is a continuous function between the topological spaces.
|
ContinuousAt.snd''
theorem ContinuousAt.snd'' :
∀ {X : Type u} {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f : Y → Z} {x : X × Y}, ContinuousAt f x.2 → ContinuousAt (fun x => f x.2) x
The theorem `ContinuousAt.snd''` states that for any three types `X`, `Y`, and `Z`, given topologies on each, and a function `f` from `Y` to `Z`, if `f` is continuous at the second component of a point `x` in the product space `X × Y`, then the function obtained by precomposing `f` with the projection onto the second component (`Prod.snd`) is also continuous at `x`. In mathematical terms, if we have a point $(x_1, y)$ in the product space and a function $f$ is continuous at $y$, then the function that maps every pair $(x', y')$ to $f(y')$ is continuous at $(x_1, y)$.
More concisely: If a function between two topological spaces is continuous at a point in its domain when viewed through the second projection, then the composition of the function with the second projection is also continuous at that point in the product space.
|
Mathlib.Topology.Constructions._auxLemma.35
theorem Mathlib.Topology.Constructions._auxLemma.35 :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set (X ⊕ Y)},
IsOpen s = (IsOpen (Sum.inl ⁻¹' s) ∧ IsOpen (Sum.inr ⁻¹' s))
This theorem states that for any two types `X` and `Y` equipped with topological spaces, and any set `s` in the sum type `X ⊕ Y`, `s` is open if and only if both the preimage of `s` under the left injection (`Sum.inl`) and the preimage of `s` under the right injection (`Sum.inr`) are open. In other words, a set in the disjoint union of two topological spaces is open if it's "open from both sides", i.e., its preimage under both the left and right injections are open.
More concisely: A subset of the disjoint union of two topological spaces is open if and only if its preimages under the left and right injections are open.
|
DenseRange.prod_map
theorem DenseRange.prod_map :
∀ {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] {ι : Type u_5}
{κ : Type u_6} {f : ι → Y} {g : κ → Z}, DenseRange f → DenseRange g → DenseRange (Prod.map f g)
The theorem `DenseRange.prod_map` states that if `f` and `g` are functions from types `ι` and `κ` to topological spaces `Y` and `Z` respectively, and both these functions have a dense range, then the function `Prod.map f g` also has a dense range. Here, `Prod.map f g` is a function that operates on pairs from `ι × κ` and produces pairs in `Y × Z` by applying `f` to the first component of the input pair and `g` to the second component. A dense range means that the closure of the set of all output values of the function is the entire space. In mathematical terms, if the images of `f` and `g` densely populate their respective spaces, then the pairs formed by `f` and `g` densely populate the product space.
More concisely: If functions `f : ι → Y` and `g : κ → Z` with dense ranges map `Prod.map f g : ι × κ → Y × Z` also has a dense range.
|
continuous_inf_dom_left₂
theorem continuous_inf_dom_left₂ :
∀ {X : Type u_5} {Y : Type u_6} {Z : Type u_7} {f : X → Y → Z} {ta1 ta2 : TopologicalSpace X}
{tb1 tb2 : TopologicalSpace Y} {tc1 : TopologicalSpace Z},
(Continuous fun p => f p.1 p.2) → Continuous fun p => f p.1 p.2
This theorem states that for any types `X`, `Y`, `Z`, and any binary function `f` from `X` and `Y` to `Z`, and given topological spaces `ta1`, `ta2` over `X`, `tb1`, `tb2` over `Y` and `tc1` over `Z`, if the function `(p => f p.1 p.2)` is continuous, then the same function `(p => f p.1 p.2)` is also continuous. This theorem is a version of the `continuous_inf_dom_left` theorem, but adapted for binary functions.
More concisely: For any types X, Y, Z and binary function f : X -> Y -> Z, and topological spaces ta over X, tb over Y, and tc over Z, if the function (p => f (x p) (y p)) is continuous, then it is also continuous.
|
continuous_pi_iff
theorem continuous_pi_iff :
∀ {X : Type u} {ι : Type u_5} {π : ι → Type u_6} [inst : TopologicalSpace X] [T : (i : ι) → TopologicalSpace (π i)]
{f : X → (i : ι) → π i}, Continuous f ↔ ∀ (i : ι), Continuous fun a => f a i
The theorem `continuous_pi_iff` states that for all types `X` and `ι`, and a type-dependent function `π : ι → Type`, given `X` and each `π i` have a topological space structure, a function `f` from `X` to each `π i` is continuous if and only if for each `i : ι`, the function `fun a => f a i` is continuous. Here, `fun a => f a i` is a function taking an element from `X` and returning an element from the type `π i`. This theorem provides a characterization of the continuity of functions into product spaces in terms of the continuity of their coordinate functions.
More concisely: A function from a topological space to a product of types, each with its own topological space structure, is continuous if and only if the function's projection to each factor space is continuous.
|
Filter.Tendsto.prod_mk_nhds
theorem Filter.Tendsto.prod_mk_nhds :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {γ : Type u_5} {x : X} {y : Y}
{f : Filter γ} {mx : γ → X} {my : γ → Y},
Filter.Tendsto mx f (nhds x) →
Filter.Tendsto my f (nhds y) → Filter.Tendsto (fun c => (mx c, my c)) f (nhds (x, y))
The theorem `Filter.Tendsto.prod_mk_nhds` states that for all types `X`, `Y`, `γ` with `X` and `Y` being topological spaces, for any points `x` in `X` and `y` in `Y`, for any filter `f` on `γ`, and for mappings `mx` from `γ` to `X` and `my` from `γ` to `Y`, if `mx` tends to `x` with respect to `f` and `my` tends to `y` with respect to `f`, then the function that sends each element `c` of `γ` to the pair `(mx c, my c)` also tends towards `(x, y)` with respect to `f`. This is essentially saying that the limit of a pair of functions is the pair of the limits, when those limits exist in the topologies of `X` and `Y`.
More concisely: Given topological spaces X and Y, points x in X and y in Y, filters f on a Common limit γ, and functions mx : γ → X and my : γ → Y with mx tending to x and my tending to y with respect to f, then the function sending c in γ to (mx c, my c) tends to (x, y) with respect to f.
|
Continuous.restrict
theorem Continuous.restrict :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X}
{t : Set Y} (h1 : Set.MapsTo f s t), Continuous f → Continuous (Set.MapsTo.restrict f s t h1)
This theorem states that for any two types `X` and `Y`, which both have a topological space structure, and for any function `f` from `X` to `Y`, if `f` maps a set `s` in `X` to a set `t` in `Y` (which means that the image of `s` under `f` is contained in `t`), then if `f` is continuous, the function derived by restricting the domain of `f` to `s` and the codomain to `t` is also continuous.
More concisely: If `X` and `Y` are topological spaces, `f: X → Y` is continuous, and `s ⊆ X` maps to `t ⊆ Y`, then the restriction of `f` to `s` and `t` is continuous.
|