Specializes.mem_open
theorem Specializes.mem_open :
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {s : Set X}, x ⤳ y → IsOpen s → y ∈ s → x ∈ s
This theorem, named `Specializes.mem_open`, is about topological spaces and the concept of specialization. It states that, for any type `X` that has a topological space structure, and for any two elements `x` and `y` of type `X`, if `x` specializes to `y` (denoted as `x ⤳ y`), and if a set `s` of elements of type `X` is open in this topological space and contains `y`, then `s` must also contain `x`. In other words, if `x` specializes to `y` and `y` belongs to an open set, then `x` will also belong to that open set.
More concisely: If `x ⤳ y` and `y ∈ s`, then `x ∈ s` for any open set `s` in a topological space `X`.
|
Inducing.specializes_iff
theorem Inducing.specializes_iff :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y},
Inducing f → (f x ⤳ f y ↔ x ⤳ y)
This theorem states that for any two types `X` and `Y` with topological space structures, any two elements `x` and `y` of `X`, and any function `f` from `X` to `Y` that induces the topology of `Y` from `X`, the specialization preorder (denoted by `⤳`) of the images `f(x)` and `f(y)` in `Y` is equivalent to the specialization preorder of `x` and `y` in `X`. The specialization preorder is a way of saying that one point is "closer" to a given set than another point, in the context of topological spaces.
More concisely: For any topological spaces X and Y, continuous functions f : X -> Y, and elements x, y in X, the specialization preorders x ⤳ S and f(x) ⤳ f[S] agree for any set S in X, where ⤳ denotes the specialization preorder.
|
Continuous.specialization_monotone
theorem Continuous.specialization_monotone :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
Continuous f → Monotone f
This theorem states that for any types `X` and `Y` with corresponding topological spaces, any continuous function `f` from `X` to `Y` is monotone. In other words, if `X` and `Y` are topological spaces and `f` is a function from `X` to `Y` that is continuous, then `f` preserves the order: for any two elements `a` and `b` in `X` such that `a` is less than or equal to `b`, the value of `f` at `a` is less than or equal to the value of `f` at `b`. This theorem establishes a link between the continuity of a function in topological spaces and its monotonicity.
More concisely: If `X` and `Y` are topological spaces and `f : X → Y` is a continuous function, then `f` is monotone, i.e., for all `a ≤ b` in `X`, we have `f(a) ≤ f(b)` in `Y`.
|
Inseparable.mem_open_iff
theorem Inseparable.mem_open_iff :
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {s : Set X}, Inseparable x y → IsOpen s → (x ∈ s ↔ y ∈ s)
This theorem states that for any given topological space 'X', if two points 'x' and 'y' within that space are inseparable (i.e., they have the same neighborhood), then for any open set 's', 'x' is a member of 's' if and only if 'y' is a member of 's'. This condition holds true for any open set 's' in the topology, provided 'x' and 'y' are inseparable and 's' is an open set. In other words, inseparable points 'x' and 'y' in a topological space share the same membership properties for open sets.
More concisely: For any topological space 'X' and inseparable points 'x' and 'y' in 'X', they belong to the same open sets.
|
SeparationQuotient.mk_eq_mk
theorem SeparationQuotient.mk_eq_mk :
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X},
SeparationQuotient.mk x = SeparationQuotient.mk y ↔ Inseparable x y
The theorem `SeparationQuotient.mk_eq_mk` states that for any topological space `X` and any two points `x` and `y` in `X`, the natural map from `X` to its separation quotient applied to `x` is equal to the same map applied to `y` if and only if `x` and `y` are inseparable. Here, two points `x` and `y` are said to be inseparable if their neighborhood filters, denoted `𝓝 x` and `𝓝 y` respectively, are equal.
More concisely: For any topological space X and points x, y in X, the natural map from X to its separation quotient takes x to y if and only if the neighborhood filters of x and y are equal.
|
Inducing.inseparable_iff
theorem Inducing.inseparable_iff :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y},
Inducing f → (Inseparable (f x) (f y) ↔ Inseparable x y)
The theorem `Inducing.inseparable_iff` states that for any two points `x` and `y` in a topological space `X` and a function `f` from `X` to another topological space `Y` that induces the topology of `Y`, the points `f(x)` and `f(y)` in `Y` are inseparable if and only if the original points `x` and `y` in `X` are inseparable. In other words, the property of being inseparable is preserved under topology-inducing functions between two topological spaces. Here, inseparable points are those for which the neighborhoods around them in the topological space are the same.
More concisely: For any topology-inducing function `f` between topological spaces `X` and `Y`, and any points `x` and `y` in `X`, `x` and `y` are inseparable in `X` if and only if `f(x)` and `f(y)` are inseparable in `Y`.
|
Specializes.pure_le_nhds
theorem Specializes.pure_le_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y → pure x ≤ nhds y := by
sorry
This theorem, named `Specializes.pure_le_nhds`, states that for any topological space `X` and any two elements `x` and `y` of `X`, if `x` specializes to `y` (denoted `x ⤳ y`), then the principal filter generated by `x` (denoted `pure x`) is less than or equal to the neighborhood filter at `y` (denoted `nhds y`). In other words, if `x` is inside every open set that contains `y`, then every neighborhood of `x` is also a neighborhood of `y`.
More concisely: For any topological space X and elements x, y of X, if x specializes to y (x ⤳ y), then the filter generated by x (pure x) is contained in the neighborhood filter at y (nhds y).
|
Inseparable.specializes
theorem Inseparable.specializes : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable x y → x ⤳ y := by
sorry
The theorem `Inseparable.specializes` states that for any topological space `X` and any two points `x` and `y` in `X`, if `x` and `y` are inseparable (meaning the neighborhoods of `x` and `y` are the same) then `x` specializes to `y`. In the context of topological spaces, "specializes" means that every open set containing `y` also contains `x`.
More concisely: If two points `x` and `y` in a topological space `X` are inseparable, then `x` is contained in every open set containing `y`.
|
Specializes.antisymm
theorem Specializes.antisymm :
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y → y ⤳ x → Inseparable x y
The theorem `Specializes.antisymm` states that for any topological space `X` and any two points `x` and `y` in `X`, if `x` specializes to `y` and `y` specializes to `x`, then `x` and `y` are inseparable. Here, specializing to, denoted `⤳`, is a relation in topology that involves comparing the closure of the singleton sets of the points, and two points are inseparable if they have the same neighborhood system in the topological space, which is equivalent to several other properties as defined by the `Inseparable` predicate.
More concisely: If two points `x` and `y` in a topological space `X` specialized to each other (`x ⤳ y` and `y ⤳ x`), then `x` and `y` are inseparable in `X`.
|
SeparationQuotient.inducing_mk
theorem SeparationQuotient.inducing_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], Inducing SeparationQuotient.mk
This theorem states that for any type `X` equipped with a topology (denoted by `[inst : TopologicalSpace X]`), the natural map from the topological space `X` to its separation quotient (`SeparationQuotient.mk`) is an inducing function. In the context of topology, an inducing function is one that, given the topology on the target space, induces the topology on the source space. This implies that the topology on `X` is the coarsest topology making `SeparationQuotient.mk` continuous.
More concisely: Given a topological space `(X : Type)` with topology `[inst : TopologicalSpace X]`, the natural map from `X` to its separation quotient `SeparationQuotient.mk X` is a topology-inducing function.
|
Inseparable.mem_closed_iff
theorem Inseparable.mem_closed_iff :
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {s : Set X},
Inseparable x y → IsClosed s → (x ∈ s ↔ y ∈ s)
The theorem `Inseparable.mem_closed_iff` states that in any topological space, for any two points `x` and `y` that are inseparable (meaning they cannot be separated by a neighborhood, as defined by the condition `nhds x = nhds y`), and for any set `s` which is closed, `x` is in `s` if and only if `y` is in `s`. That is, membership of one of these inseparable points in the set implies membership of the other. This theorem provides a connection between inseparability of points and the properties of closed sets in a topological space.
More concisely: In any topological space, if two points are inseparable then they have identical elements in every closed set.
|
Inseparable.map
theorem Inseparable.map :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y},
Inseparable x y → Continuous f → Inseparable (f x) (f y)
The theorem `Inseparable.map` states that in any two topological spaces `X` and `Y`, for any two points `x` and `y` in `X` that are inseparable, and for any function `f` from `X` to `Y` that is continuous, the images of `x` and `y` under `f` are also inseparable in `Y`. In other words, the inseparability property of the points `x` and `y` is preserved under the continuous mapping `f`.
More concisely: For any continuous function $f$ between topological spaces $X$ and $Y$, if $x$ and $y$ in $X$ are inseparable points, then $f(x)$ and $f(y)$ are inseparable points in $Y$.
|
Inseparable.refl
theorem Inseparable.refl : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), Inseparable x x
This theorem, `Inseparable.refl`, states that for any given point 'x' in a topological space 'X', the point 'x' is inseparable from itself. In other words, in any topological space, a point is always inseparable from itself, which means the neighbourhoods of the point 'x' are always the same as the neighbourhoods of the same point 'x'.
More concisely: For any point x in a topological space, the singleton sets {x} and {x} have non-empty intersection. In Lean 4, this is expressed as the theorem `Inseparable.refl x : ∃ (U : set X), x ∈ U ∧ x ∈ U.^op`.
|
Specializes.mem_closure
theorem Specializes.mem_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y → y ∈ closure {x} := by
sorry
This theorem, referred to as `Specializes.mem_closure`, is an alias of the forward direction of another theorem called `specializes_iff_mem_closure`. It states that for any type `X`, given a topological space structure and any two elements `x` and `y` of `X`, if `x` specializes to `y` (denoted as `x ⤳ y`), then `y` is an element of the closure of the singleton set containing `x`. In other words, if `x` specializes to `y`, then `y` belongs to the smallest closed set containing `x`.
More concisely: If `x ⤳ y` in a topological space `X`, then `y` is in the closure of the singleton set `{x}`.
|
Specializes.nhds_le_nhds
theorem Specializes.nhds_le_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y → nhds x ≤ nhds y := by
sorry
This theorem, which is an alias of the forward direction of `specializes_iff_nhds`, states that for any type `X` equipped with a topological space structure and any two elements `x` and `y` of `X`, if `x` specializes to `y` (represented as `x ⤳ y`, which means every neighborhood of `y` is also a neighborhood of `x`), then the neighborhood filter at `x` is less than or equal to the neighborhood filter at `y`. In other words, every neighborhood of `x` is also a neighborhood of `y`.
More concisely: If `x` specializes to `y` in a topological space `X`, then the neighborhood filter at `x` is contained in the neighborhood filter at `y`.
|
Specializes.closure_subset
theorem Specializes.closure_subset :
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y → closure {y} ⊆ closure {x}
The theorem `Specializes.closure_subset` states that for any topological space `X` and any two elements `x` and `y` of `X`, if `x` specializes to `y` (denoted as `x ⤳ y`), then the closure of the set containing just `y` is a subset of the closure of the set containing just `x`. In other words, if `x` specializes to `y`, then any closed set that contains `y` (and possibly other elements) also contains `x`.
More concisely: For any topological space X and elements x and y with x specializing to y, the closure of {y} is contained in the closure of {x}.
|
specializes_iff_mem_closure
theorem specializes_iff_mem_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y ↔ y ∈ closure {x}
The theorem `specializes_iff_mem_closure` states that for any topological space `X` and any two points `x` and `y` in `X`, the point `x` specializes to `y` (i.e., every open neighborhood of `x` also contains `y`) if and only if `y` is a member of the closure of the set containing only `x`. In other words, the specialization relation between two points corresponds to membership in the closure of the singleton set.
More concisely: A point specializes to another point in a topological space if and only if the second point belongs to the closure of the set containing the first point.
|
SeparationQuotient.isOpenMap_mk
theorem SeparationQuotient.isOpenMap_mk :
∀ {X : Type u_1} [inst : TopologicalSpace X], IsOpenMap SeparationQuotient.mk
The theorem `SeparationQuotient.isOpenMap_mk` declares that for any topological space `X`, the natural map from `X` to its separation quotient, denoted as `SeparationQuotient.mk`, is an open map. An open map, in this context, is a function where the image of any open set in `X` is also an open set in the separation quotient of `X`.
More concisely: The natural map from a topological space to its separation quotient is an open function.
|
specializes_iff_forall_open
theorem specializes_iff_forall_open :
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y ↔ ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
This theorem, named `specializes_iff_forall_open`, states that for any topological space `X` and for any two points `x` and `y` in `X`, the condition `x` specializes to `y` is equivalent to the property that for all sets `s` in `X`, if `s` is an open set and `y` is an element of `s`, then `x` is also an element of `s`. In simpler terms, a point `x` specializes to another point `y` if and only if `x` belongs to every open set that `y` belongs to.
More concisely: A point x specializes to another point y if and only if for every open set s containing y, x belongs to s.
|
specializes_iff_pure
theorem specializes_iff_pure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y ↔ pure x ≤ nhds y := by
sorry
This theorem states that for any topological space `X` and any two points `x` and `y` from `X`, `x` specializes to `y` (notation: `x ⤳ y`) if and only if the filter of `x` is less than or equal to the neighborhood filter at `y` (notation: `pure x ≤ nhds y`). In other words, `x` is said to specialize to `y` when every neighborhood of `y` also contains `x`.
More concisely: For any topological space X and points x, y from X, x specializes to y (x ⤳ y) if and only if the filter of x is included in the neighborhood filter at y (pure x ≤ nhds y).
|
SeparationQuotient.surjective_mk
theorem SeparationQuotient.surjective_mk :
∀ {X : Type u_1} [inst : TopologicalSpace X], Function.Surjective SeparationQuotient.mk
The theorem `SeparationQuotient.surjective_mk` states that for any type `X` that has a topology defined on it, the natural map from this topological space to its separation quotient is surjective. In other words, for every element in the separation quotient of a topological space, there exists an element in the original topological space that maps to it through the natural map. The separation quotient is defined via the equivalence relation of having the same closure.
More concisely: For any topological space X, the natural map from X to its separation quotient is surjective. (Two elements in X map to the same point in the quotient if and only if they have the same closure.)
|
Specializes.map
theorem Specializes.map :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y},
x ⤳ y → Continuous f → f x ⤳ f y
This theorem states that for any two types `X` and `Y`, given that `X` and `Y` are both topological spaces, and given a function `f` from `X` to `Y` and any two elements `x` and `y` of `X`, if `x` specializes to `y` and `f` is a continuous function, then `f(x)` also specializes to `f(y)`. This theorem captures the idea that the specialization relation, which is a form of ordering in topological spaces, preserves continuity under function mapping.
More concisely: If `f` is a continuous function between topological spaces `X` and `Y`, and `x` specializes to `y` in `X`, then `f(x)` specializes to `f(y)` in `Y`.
|
SeparationQuotient.continuous_mk
theorem SeparationQuotient.continuous_mk :
∀ {X : Type u_1} [inst : TopologicalSpace X], Continuous SeparationQuotient.mk
The theorem `SeparationQuotient.continuous_mk` states that for any type `X` equipped with a topological space structure, the natural map from `X` to its separation quotient, denoted as `SeparationQuotient.mk`, is continuous. Here, continuity refers to the mathematical concept of a function maintaining closeness, which in the context of topological spaces, means that the preimage of any open set is open. The separation quotient of a topological space is a related space where indistinguishable points are identified, and the `SeparationQuotient.mk` function represents the canonical projection map to this quotient space.
More concisely: The canonical projection map from a topological space to its separation quotient is a continuous function.
|
Mathlib.Topology.Inseparable._auxLemma.10
theorem Mathlib.Topology.Inseparable._auxLemma.10 :
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable x y = (x ⤳ y ∧ y ⤳ x)
This theorem states that for any topological space `X` and any two points `x` and `y` in this space, `x` and `y` are inseparable (i.e., they share the same neighborhood structure) if and only if `x` converges to `y` and `y` converges to `x`. Here, `x ⤳ y` denotes the convergence of `x` to `y`, meaning every neighborhood of `y` contains `x` after a certain point in a sequence or function, and similarly for `y ⤳ x`.
More concisely: For any topological space X and points x, y in X, x and y are inseparable if and only if they converge to each other, i.e., x ⤳ y and y ⤳ x.
|
specializes_rfl
theorem specializes_rfl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, x ⤳ x
This theorem, "specializes_rfl," states that for every type `X` equipped with a topological space structure, and for any element `x` of `X`, `x` specializes to itself. In other words, for any point in a given topological space, the specialization relation is reflexive. This relation essentially establishes that the closure of the set containing the point includes the point itself.
More concisely: For every topological space (X, top), and for all x ∈ X, x belongs to the closure of {x}.
|
specializes_TFAE
theorem specializes_TFAE :
∀ {X : Type u_1} [inst : TopologicalSpace X] (x y : X),
[x ⤳ y, pure x ≤ nhds y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)].TFAE
This theorem provides a collection of equivalent definitions for the relation "x specializes to y" (denoted `x ⤳ y`) in a topological space `X`. Specifically, the following properties are equivalent:
1. `x` specializes to `y` (`x ⤳ y`).
2. The filter generated by the single point set `{x}` is less than or equal to the neighborhood filter at `y` (`pure x ≤ nhds y`).
3. For any open set `s` that contains `y`, `x` is also in `s` (`∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s`).
4. For any closed set `s` that contains `x`, `y` is also in `s` (`∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s`).
5. `y` is in the closure of the set `{x}` (`y ∈ closure {x}`).
6. The closure of the set `{y}` is a subset of the closure of the set `{x}` (`closure {y} ⊆ closure {x}`).
7. `y` is a cluster point of the filter generated by the single point `{x}` (`ClusterPt y (pure x)`).
In other words, these seven conditions are equivalent ways of saying that `x` specializes to `y`.
More concisely: In a topological space, the following seven conditions are equivalent: `x ⤳ y` if and only if (i) `pure x ≤ nhds y`, (ii) `x ∈ s` for all open sets `s` containing `y`, (iii) `y ∈ s` for all closed sets `s` containing `x`, (iv) `y ∈ closure {x}`, (v) `closure {y} ⊆ closure {x}`, (vi) `ClusterPt y (pure x)`, where `x ⤳ y` denotes the relation "`x` specializes to `y`".
|