OnePoint.isOpen_compl_image_coe
theorem OnePoint.isOpen_compl_image_coe :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsOpen (OnePoint.some '' s)ᶜ ↔ IsClosed s ∧ IsCompact s
The theorem `OnePoint.isOpen_compl_image_coe` states that for any type `X` with a topology and a set `s` of `X`, the set complement of the image of `s` under the `OnePoint.some` function is open if and only if the set `s` is both closed and compact in the topological space `X`. In other words, the image of `s` under `OnePoint.some` has an open complement if and only if `s` is a compact and closed set in the topological space.
More concisely: The set complement of the image of a compact and closed set `s` in a topological space under the `OnePoint.some` function is open.
|
Mathlib.Topology.Compactification.OnePoint._auxLemma.2
theorem Mathlib.Topology.Compactification.OnePoint._auxLemma.2 :
∀ {X : Type u_1} (x : X), (↑x = OnePoint.infty) = False
This theorem states that for any type `X` and any element `x` of `X`, the assertion that `x` is equal to the point at infinity is always false. In other words, no standard point from the original space `X` can be equal to the added point at infinity in the one-point compactification of `X`.
More concisely: For any type X and its element x, x is not equal to the point at infinity in the one-point compactification of X.
|
OnePoint.openEmbedding_coe
theorem OnePoint.openEmbedding_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X], OpenEmbedding OnePoint.some := by
sorry
This theorem states that for any type `X` equipped with a topological space structure, the function `OnePoint.some`, which coerces an element of `X` into an element of `OnePoint X`, is an open embedding. In the context of topology, an open embedding is a type of continuous function between topological spaces that not only maps open sets to open sets, but also has the property that the image of the function is a topological space with the subspace topology inherited from the codomain.
More concisely: The `OnePoint.some` function, which maps an element of a topological space `X` to the one-point topological space on it, is a continuous open embedding.
|
Continuous.homeoOfEquivCompactToT2.t1_counterexample
theorem Continuous.homeoOfEquivCompactToT2.t1_counterexample :
∃ α β x x_1, CompactSpace α ∧ T1Space β ∧ ∃ f, Continuous ⇑f ∧ ¬Continuous ⇑f.symm
This theorem provides a concrete counterexample that demonstrates the theorem `Continuous.homeoOfEquivCompactToT2` can't be generalized from `T2Space` to `T1Space`. Here, `α` is defined as the one-point compactification of `ℕ`, and `β` is defined as the same space with the cofinite topology. Then, `α` is a compact space, `β` is a T1 space, and the identity map from `α` to `β` is a continuous equivalence but not a homeomorphism. The theorem thus states the existence of such spaces `α` and `β` and a function `f`, such that `f` is a continuous function but its inverse is not continuous.
More concisely: The theorem states that the identity map between the one-point compactification of natural numbers and the same space with the cofinite topology is a continuous equivalence but not a homeomorphism between compact and T1 spaces.
|
OnePoint.nhds_coe_eq
theorem OnePoint.nhds_coe_eq :
∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), nhds ↑x = Filter.map OnePoint.some (nhds x)
The theorem `OnePoint.nhds_coe_eq` states that for any type `X` with a topology and any element `x` from `X`, the neighborhood filter of the embedded point `x` in the one-point compactification of `X` (represented by `↑x`) is equivalent to the image of the neighborhood filter of `x` under the map `OnePoint.some`. In other words, the neighborhoods of `x` in the extended space are the same as the images of the neighborhoods of `x` in the original space under the embedding `OnePoint.some`.
More concisely: The neighborhood filter of an element `x` in the one-point compactification of a topological space `X` is equal to the image of the neighborhood filter of `x` in `X` under the embedding `OnePoint.some`.
|
OnePoint.coe_injective
theorem OnePoint.coe_injective : ∀ {X : Type u_1}, Function.Injective OnePoint.some
This theorem asserts that for every type `X`, the function `OnePoint.some` is injective. In other words, if we apply this function to two elements of `X` and get the same result, it means that the two elements were actually identical. Put into a mathematical context, given any type `X`, this function maps each element to a unique element in the `OnePoint X` type, hence preserving distinctness.
More concisely: For every type X, the function OnePoint.some from X to OnePoint X is a bijection (injective and surjective).
|
OnePoint.compl_range_coe
theorem OnePoint.compl_range_coe : ∀ {X : Type u_1}, (Set.range OnePoint.some)ᶜ = {OnePoint.infty}
The theorem `OnePoint.compl_range_coe` states that for any type `X`, the complement of the range of the function `OnePoint.some` (which coerces elements of type `X` to `OnePoint X`) is the set containing only the element `OnePoint.infty`. In other words, `OnePoint.infty` is the only element of the type `OnePoint X` that is not the image of any element from `X` under the function `OnePoint.some`.
More concisely: The theorem `OnePoint.compl_range_coe` asserts that the complement of the image of `X` under `OnePoint.some` in `OnePoint X` consists only of `OnePoint.infty`.
|
OnePoint.not_continuous_cofiniteTopology_of_symm
theorem OnePoint.not_continuous_cofiniteTopology_of_symm :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Infinite X] [inst_2 : DiscreteTopology X],
¬Continuous ⇑CofiniteTopology.of.symm
This theorem states that for any infinite type `X` with a discrete topology (for example, the natural numbers `ℕ`), the identity map from `CofiniteTopology (OnePoint X)` to `OnePoint X` is not continuous. In other words, if we have a topological space `X` that is infinite and discrete, then the inverse of the identity equivalence (established by `CofiniteTopology.of`) that maps elements from `CofiniteTopology (OnePoint X)` to `OnePoint X` does not preserve the continuity property.
More concisely: The identity map from `CofiniteTopology (OnePoint X)` to `OnePoint X` is not continuous for any infinite, discrete topological space `X`.
|
OnePoint.isOpen_iff_of_mem
theorem OnePoint.isOpen_iff_of_mem :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set (OnePoint X)},
OnePoint.infty ∈ s → (IsOpen s ↔ IsClosed (OnePoint.some ⁻¹' s)ᶜ ∧ IsCompact (OnePoint.some ⁻¹' s)ᶜ)
The theorem `OnePoint.isOpen_iff_of_mem` states that for any topological space `X` and any set `s` of the one-point extension of `X` where the point at infinity is a member of `s`, then `s` is open if and only if the preimage of `s` under the embedding of `X` into its one-point extension, denoted as `OnePoint.some`, is closed and compact. The preimage of `s` is the subset of `X` that is mapped to `s` by `OnePoint.some`, and the notation `(OnePoint.some ⁻¹' s)ᶜ` means the complement of this preimage, i.e., the set of all points in `X` not in this preimage. The theorem essentially connects the openness of a set in the one-point extension of a topological space with the closure and compactness of a related set in the original space.
More concisely: A set in the one-point extension of a topological space is open if and only if its preimage under the embedding is closed and compact.
|
OnePoint.nhds_infty_eq
theorem OnePoint.nhds_infty_eq :
∀ {X : Type u_1} [inst : TopologicalSpace X],
nhds OnePoint.infty = Filter.map OnePoint.some (Filter.coclosedCompact X) ⊔ pure OnePoint.infty
This theorem states that for any type `X` with a topological space structure, the neighborhood filter at the point at infinity is equal to the sup (join operation in filter lattice) of the forward map of the filter generated by complements to closed compact sets in `X` under the coercion from `X` to `OnePoint X`, and the filter containing only the point at infinity. In other words, it describes how the neighborhoods of the point at infinity in the extended space `OnePoint X` are related to the compact closed subsets of the original space `X`.
More concisely: The neighborhood filter at the point at inity in the one-point compactification of a topological space `X` is equal to the join of the filter generated by complements of closed compact sets in `X`, and the filter containing only the point at infinity.
|
OnePoint.infty_not_mem_image_coe
theorem OnePoint.infty_not_mem_image_coe : ∀ {X : Type u_1} {s : Set X}, OnePoint.infty ∉ OnePoint.some '' s
This theorem states that, for any type `X` and any set `s` of elements of type `X`, the point at infinity (represented as `OnePoint.infty`) is not a member of the image of the set `s` under the function `OnePoint.some`. In other words, if we apply the `OnePoint.some` function to each element in the set `s` to obtain a new set, this new set will not contain the point at infinity.
More concisely: For any set `s` of elements from type `X`, the image of `s` under the function `OnePoint.some` does not contain the point at infinity `OnePoint.infty`.
|
OnePoint.denseRange_coe
theorem OnePoint.denseRange_coe :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : NoncompactSpace X], DenseRange OnePoint.some
This theorem states that if `X` is a topological space that is not compact, then the natural embedding from `X` to its one-point compactification, denoted as `OnePoint X`, has a dense range. In other words, the image of any element in `X` under the natural embedding `OnePoint.some` is a dense subset of the space `OnePoint X`. This means every open subset of `OnePoint X` contains at least one point from the range of the embedding, or equivalently, the closure of the image of the embedding is the entire space `OnePoint X`.
More concisely: If `X` is a non-compact topological space, the image of `X` under its natural embedding into its one-point compactification is dense in the compactification.
|