LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Topology.Separation

`separatedNhds_of_isCompact_isClosed` theorem separatedNhds_of_isCompact_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : RegularSpace X] {s t : Set X}, IsCompact s → IsClosed t → Disjoint s t → SeparatedNhds s t This theorem states that in a regular topological space, given a compact set `s` and a closed set `t`, if these sets are disjoint (i.e., they have no elements in common), then there exist two open neighborhoods `U` of `s` and `V` of `t` that are also disjoint. This property is a characteristic of regular spaces, and it encapsulates the intuitive idea that compact sets can be "separated" from closed sets by open sets, a property that can be visualized in Euclidean spaces. More concisely: In a regular topological space, given a compact and a closed disjoint set, there exist open neighborhoods of each that are also disjoint.
`IsClosed.exists_closed_singleton` theorem IsClosed.exists_closed_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T0Space X] [inst_2 : CompactSpace X] {S : Set X}, IsClosed S → S.Nonempty → ∃ x ∈ S, IsClosed {x} The theorem `IsClosed.exists_closed_singleton` states that for any closed set `S` in a compact T0 space (a topological space with the T0 separation axiom), there exists an element `x` in `S` such that the set `{x}` is closed. In other words, in a compact T0 space, every closed set has at least one element that forms a closed singleton set. More concisely: In a compact T0 space, every closed set contains at least one point that forms a closed singleton.
`separatedNhds_of_isCompact_isCompact_isClosed` theorem separatedNhds_of_isCompact_isCompact_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {K L : Set X}, IsCompact K → IsCompact L → IsClosed L → Disjoint K L → SeparatedNhds K L The theorem `separatedNhds_of_isCompact_isCompact_isClosed` states that in an R₁ topological space, if `K` and `L` are two disjoint compact sets and `L` is also a closed set, then there exist disjoint neighborhoods for `K` and `L`. In other words, there are two open sets, one containing all points of `K` and the other containing all points of `L`, such that these two open sets do not intersect. This is a property of separation in topological spaces, specifically pertaining to compact and closed sets. More concisely: In an R₁ topological space, disjoint compact and closed sets have disjoint open neighborhoods.
`exists_open_between_and_isCompact_closure` theorem exists_open_between_and_isCompact_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LocallyCompactSpace X] [inst_2 : RegularSpace X] {K U : Set X}, IsCompact K → IsOpen U → K ⊆ U → ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V) The theorem `exists_open_between_and_isCompact_closure` states that in a locally compact regular topological space, if we are given a compact set `K` that is a subset of an open set `U`, there exists an open set `V` such that `K` is a subset of `V` and the closure of `V` is a subset of `U` as well as being compact. In other words, we can always find an open set `V` which lies between the compact set `K` and the open set `U`, and whose closure is compact and lies within `U`. More concisely: In a locally compact regular topological space, given a compact subset `K` of an open set `U`, there exists an open set `V` such that `K` is subset of `V` and the compact closure of `V` is a subset of `U`.
`isOpen_inter_eq_singleton_of_mem_discrete` theorem isOpen_inter_eq_singleton_of_mem_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [inst_1 : DiscreteTopology ↑s] {x : X}, x ∈ s → ∃ U, IsOpen U ∧ U ∩ s = {x} This theorem states that for any topological space `X` and for a specific point `x` in a discrete subset `s` of `X`, there exists an open set `U` such that `U` is open in the topological space `X`, and the intersection of `U` and `s` is a singleton set that only contains the point `x`. This encapsulates the intuitive idea that in a discrete space, each point can be "isolated" with an open set. More concisely: In a discrete topological space, every point in a subset has a neighborhood that contains only that point.
`ClosedEmbedding.t4Space` theorem ClosedEmbedding.t4Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T4Space Y] {f : X → Y}, ClosedEmbedding f → T4Space X This theorem states that, for any two types `X` and `Y` with defined topological structures, and a function `f` from `X` to `Y`, if `Y` is a T₄ space (also known as a normal Hausdorff space), and if `f` is a closed embedding (i.e., a function that is continuous, injective, and the image of `f` is a closed set in `Y`), then `X` is also a T₄ space. In other words, the property of being a T₄ space is preserved under closed embeddings. More concisely: If `X` and `Y` are types with topological structures, `f : X → Y` is a closed embedding with `Y` being a T₄ space, then `X` is also a T₄ space.
`Mathlib.Topology.Separation._auxLemma.47` theorem Mathlib.Topology.Separation._auxLemma.47 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : T1Space X] {l : Filter Y} [inst_2 : l.NeBot] {c d : X}, Filter.Tendsto (fun x => c) l (nhds d) = (c = d) The theorem `Mathlib.Topology.Separation._auxLemma.47` states that for any two points `c` and `d` in a T1 topological space `X`, and for a non-bottom filter `l` on some type `Y`, the function that is constantly `c` tends to `d` with respect to the filter `l` if and only if `c` equals `d`. In other words, a constant function at `c` has a limit of `d` with respect to filter `l` if and only if `c` equals `d`. This limit is considered in the filter-topology framework, where the limit of the function is defined by the `Filter.Tendsto` predicate. More concisely: In a T1 topological space, a constant function with respect to two points `c` and `d` has a limit converging to `d` with respect to a non-bottom filter `l` if and only if `c` equals `d`.
`not_preirreducible_nontrivial_t2` theorem not_preirreducible_nontrivial_t2 : ∀ (X : Type u_4) [inst : TopologicalSpace X] [inst_1 : PreirreducibleSpace X] [inst_2 : Nontrivial X] [inst : T2Space X], False This theorem states that there cannot exist a nontrivial preirreducible T₂ (also known as Hausdorff) topological space. In other words, if we have a topological space that is both preirreducible (meaning that the space cannot be covered by two disjoint open sets) and Hausdorff (meaning any two distinct points in the space can be separated by neighbourhoods), then this space cannot be nontrivial (i.e., it must contain at most one point). More concisely: A preirreducible and Hausdorff topological space is a singleton.
`isOpen_ne` theorem isOpen_ne : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] {x : X}, IsOpen {y \| y ≠ x} := by sorry This theorem states that for any type `X` equipped with a topological space structure and T1 space structure (i.e., every singleton set is closed), and for any element `x` of type `X`, the set of all elements `y` in `X` that are not equal to `x` is an open set in the given topological space. In other words, the complement of the singleton set containing `x` is an open set. More concisely: For any T1 topological space `(X, τ)` and its element `x ∈ X`, the complement of the singleton set `{x}` is an open set in `X`.
`specializes_iff_inseparable` theorem specializes_iff_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R0Space X] {x y : X}, x ⤳ y ↔ Inseparable x y In a space that satisfies the R0 separation axiom (R0 space), the property of one point specializing to another is equivalent to the two points being inseparable. Here, a point 'x' is said to specialize to 'y' (denoted as 'x ⤳ y') if 'y' belongs to the closure of the singleton set containing 'x'. On the other hand, two points 'x' and 'y' are inseparable if their respective neighborhoods are equal (in terms of sets in the topological space), or equivalently, 'x' belongs to every open set that 'y' belongs to and vice versa. More concisely: In an R0 space, a point specializes to another if and only if they are inseparable.
`loc_compact_Haus_tot_disc_of_zero_dim` theorem loc_compact_Haus_tot_disc_of_zero_dim : ∀ {H : Type u_3} [inst : TopologicalSpace H] [inst_1 : LocallyCompactSpace H] [inst_2 : T2Space H] [inst_3 : TotallyDisconnectedSpace H], TopologicalSpace.IsTopologicalBasis {s \| IsClopen s} The theorem states that in a space which is both locally compact and Hausdorff, and also totally disconnected, there exists a topological basis consisting of clopen sets. Here, a Hausdorff space is one where any two distinct points can be separated by open sets, a totally disconnected space is one where there is no non-trivial connected subset, and a locally compact space is one where every point has a compact neighbourhood. A clopen set is one that is both closed and open. A topological basis for a topological space is a collection of open sets such that any open set can be written as a union of sets from the collection. More concisely: In a locally compact and Hausdorff totally disconnected space, there exists a topological basis consisting of clopen sets.
`exists_mem_nhds_isClosed_subset` theorem exists_mem_nhds_isClosed_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : RegularSpace X] {x : X} {s : Set X}, s ∈ nhds x → ∃ t ∈ nhds x, IsClosed t ∧ t ⊆ s This theorem states that for any topological space `X` that also has the property of being a regular space, for any element `x` from `X` and for any set `s` of elements from `X` that is a neighborhood of `x`, there exists a subset `t` that is also a neighborhood of `x`, is a closed set in the topological sense, and is a subset of `s`. The theorem is expressing a property related to the interaction of open and closed sets in a regular space, a type of topological space with certain separation properties. More concisely: In a regular topological space, for every point `x` and neighboring open set `s`, there exists a closed neighborhood `t` of `x` contained in `s`.
`Set.Finite.isClosed` theorem Set.Finite.isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] {s : Set X}, s.Finite → IsClosed s This theorem states that for any given type `X` that is a topological space and satisfies the T1 separation axiom, any finite set `s` of elements of type `X` is a closed set. In other words, in a T1 topological space, finite sets are always closed. In this context, being "closed" is a property of sets that relates to the concept of limit points in topology. Specifically, a set is closed if it contains all of its limit points. More concisely: In a T1 topological space, every finite subset is a closed set.
`t0Space_iff_inseparable` theorem t0Space_iff_inseparable : ∀ (X : Type u) [inst : TopologicalSpace X], T0Space X ↔ ∀ (x y : X), Inseparable x y → x = y The theorem `t0Space_iff_inseparable` states that for any topological space `X`, `X` is a T0-space (also known as a Kolmogorov space) if and only if for any two points `x` and `y` in `X`, if `x` and `y` are inseparable (meaning the neighborhoods of `x` and `y` are identical), then `x` must be equal to `y`. This theorem thus establishes a connection between the topological property of being a T0-space and the notion of inseparability of points in that space. More concisely: A topological space is T0 (Kolmogorov) if and only if inseparable points are equal.
`Inducing.injective` theorem Inducing.injective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T0Space X] {f : X → Y}, Inducing f → Function.Injective f The theorem `Inducing.injective` states that for all types `X` and `Y`, if `X` is equipped with a `TopologicalSpace` structure and `T0Space` (also known as a Kolmogorov space, where any two distinct points in the space are topologically distinguishable) structure, and `Y` is equipped with a `TopologicalSpace` structure, then for any function `f` from `X` to `Y` that induces the topology on `X` from `Y`, this function `f` is injective. In other words, if `f` preserves the topological structure and `X` is a `T0Space`, then `f` is such that if `f x = f y` then `x = y`. More concisely: If X is a T0 space and has the topology induced from a topological space Y via a function f, then f is injective.
`specializes_comm` theorem specializes_comm : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R0Space X] {x y : X}, x ⤳ y ↔ y ⤳ x This theorem states that in a particular type of topological space called an R₀ space, the "specializes" relation is symmetric. In other words, for any two points `x` and `y` in this space, if `x` specializes to `y` then `y` also specializes to `x`, and vice versa. More concisely: In an R₀ space, the "specialized to" relation is a symmetric relation between points.
`exists_open_with_compact_closure` theorem exists_open_with_compact_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] [inst_2 : WeaklyLocallyCompactSpace X] (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U) This theorem, named `exists_open_with_compact_closure`, states that in a weakly locally compact R₁ space, every point has an open neighborhood whose closure is compact. Specifically, for every type `X` that has a topological space structure and is a weakly locally compact R₁ space, for any point `x` in `X`, there exists a set `U` which is open, contains `x`, and the closure of `U` is compact. More concisely: In a weakly locally compact R₁ space, every point has an open neighborhood with compact closure.
`t1Space_TFAE` theorem t1Space_TFAE : ∀ (X : Type u) [inst : TopologicalSpace X], [T1Space X, ∀ (x : X), IsClosed {x}, ∀ (x : X), IsOpen {x}ᶜ, Continuous ⇑CofiniteTopology.of, ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ nhds x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ nhds x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (nhds x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (nhds y), ∀ ⦃x y : X⦄, x ⤳ y → x = y].TFAE The theorem `t1Space_TFAE` states that for any type `X` equipped with a `TopologicalSpace` structure, the following propositions are equivalent: 1. `X` is a T1 space, which means that for any two different points, each has a neighborhood not containing the other. 2. Every single-point set `{x}` is closed. 3. The complement of every single-point set `{x}` is open. 4. The identity function from `X` to its cofinite topology is continuous. 5. For any two different points `x` and `y`, the set containing all points except `y` is a neighborhood of `x`. 6. For any two different points `x` and `y`, there exists some set `s` which is a neighborhood of `x` but `y` is not in `s`. 7. For any two different points `x` and `y`, there exists an open set `U` which contains `x` but not `y`. 8. For any two different points `x` and `y`, the neighborhood filters at `x` and `y` are disjoint. 9. For any two different points `x` and `y`, the neighborhood filter at `y` and the principal filter generated by `x` are disjoint. 10. For any two different points `x` and `y`, if `x` is related to `y` by a certain relation (encoded by `x ⤳ y`), then `x` must be equal to `y`. In the context of topology, these propositions are all different ways of expressing the property of being a T1 space, hence they are all equivalent. More concisely: A topological space `X` is T1 if and only if for any two distinct points `x` and `y`, there exist disjoint open sets containing each point.
`point_disjoint_finset_opens_of_t2` theorem point_disjoint_finset_opens_of_t2 : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {x : X} {s : Finset X}, x ∉ s → SeparatedNhds {x} ↑s The theorem `point_disjoint_finset_opens_of_t2` states that for any topological space `X` which is also a T2 space (also known as a Hausdorff space), any element `x` of `X`, and any finite set `s` of elements of `X`, if `x` is not an element of `s`, then the single-element set `{x}` and the set `s` are "separated" in the sense defined by the `SeparatedNhds` predicate. In other words, there exist two open sets `U` and `V` in the space such that `U` contains `x`, `V` contains all elements of `s`, and `U` and `V` are disjoint. This is a special case of a property that holds in all T2 spaces: any two distinct points can be separated by disjoint open sets. More concisely: In a T2 (Hausdorff) space, for any point not in a finite set, there exist disjoint open sets containing each respectively.
`SeparatedNhds.disjoint_nhdsSet` theorem SeparatedNhds.disjoint_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → Disjoint (nhdsSet s) (nhdsSet t) This theorem, referred to as an alias of the forward direction of `separatedNhds_iff_disjoint`, establishes the relationship between separated neighborhoods and disjoint neighborhood sets in a given topological space. Specifically, for any topological space `X` and any two subsets `s` and `t` of `X`, if `s` and `t` are separated neighborhoods (i.e., they can be enclosed in disjoint open sets), then the filter of neighborhoods of `s` and the filter of neighborhoods of `t` are disjoint. In other words, there does not exist any element in the topological space `X` that belongs to both `nhdsSet s` and `nhdsSet t`. More concisely: If two subsets of a topological space are separated neighborhoods, then their neighborhood filters are disjoint.
`t1Space_iff_specializes_imp_eq` theorem t1Space_iff_specializes_imp_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X], T1Space X ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y This theorem states that for any type `X` equipped with a topological space structure, `X` is a T1 space if and only if for any two elements `x` and `y` in `X`, the specialization relation `x ⤳ y` implies that `x` equals `y`. The specialization relation is a fundamental concept in topology which intuitively says that a point `x` is "closer" than or "specializes" to a point `y` if every open set containing `y` also contains `x`. In a T1 space, distinct points are topologically distinguishable. More concisely: A topological space `X` is T1 if and only if the specialization relation `x ⤳ y` implies `x = y` for all `x, y ∈ X`.
`Embedding.t3Space` theorem Embedding.t3Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T3Space Y] {f : X → Y}, Embedding f → T3Space X The theorem states that for any two types `X` and `Y`, each with an associated topological space, and given `Y` is a T3 space (also known as a regular T1 space, which means any two disjoint closed sets can be separated by two disjoint open sets), if there exists an embedding function `f` from `X` to `Y` (that is, `f` is injective and the topology on `X` is the initial topology with respect to `f` and the topology on `Y`), then `X` is also a T3 space. More concisely: If `X` and `Y` are types with topologies, `Y` is a T3 space, and there exists an embedding `f : X ↪ Y`, then `X` is also a T3 space.
`connectedComponent_eq_iInter_isClopen` theorem connectedComponent_eq_iInter_isClopen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : CompactSpace X] (x : X), connectedComponent x = ⋂ s, ↑s In a compact Hausdorff (T₂) space, the theorem states that the connected component of a point is equivalent to the intersection of all its clopen (both closed and open) neighborhoods. More specifically, for any point in such a space, the set of all points reachable from it without leaving a connected subset is the same as the set of points contained in every clopen subset that includes the point. More concisely: In a compact Hausdorff space, the connected component of a point equals the intersection of all clopen neighborhoods containing it.
`SeparatedNhds.of_isCompact_isCompact` theorem SeparatedNhds.of_isCompact_isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {s t : Set X}, IsCompact s → IsCompact t → Disjoint s t → SeparatedNhds s t This theorem states that in a topological space `X` that is also a T2 space (also known as a Hausdorff space), for any two compact sets `s` and `t` that are disjoint, it is guaranteed that there exist two open sets `U` and `V` such that `s` is a subset of `U`, `t` is a subset of `V`, and `U` and `V` are disjoint. This theorem therefore expresses a property of compact sets in a Hausdorff space, saying that they can be separated by two disjoint open sets. More concisely: In a T2 (Hausdorff) topological space, any two disjoint compact sets can be separated by two disjoint open sets.
`IsCompact.closure_subset_of_isOpen` theorem IsCompact.closure_subset_of_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {K : Set X}, IsCompact K → ∀ {U : Set X}, IsOpen U → K ⊆ U → closure K ⊆ U In a R₁ space (a topological space that satisfies the R₁ separation axiom), given a compact set `K` and an open set `U`, if `K` is a subset of `U`, then the closure of `K` is also a subset of `U`. The closure of a set is the smallest closed set that contains the original set. This theorem states that the closure of a compact set, when contained within an open set, remains within that open set in an R₁ space. More concisely: In an R₁ space, the closure of a compact set is contained in any open set that contains the set itself.
`closed_nhds_basis` theorem closed_nhds_basis : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : RegularSpace X] (x : X), (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsClosed s) id This theorem states that for any type `X`, given that `X` is a topological space and is also a regular space, and for any element `x` of `X`, the neighborhood filter at `x` has a basis formed by the sets that belong to the neighborhood of `x` and are also closed. A basis for a filter is a collection of sets such that every set in the filter contains an element of the basis. In other words, this theorem guarantees that we can always find a closed neighborhood around each point in a regular topological space. More concisely: In a regular topological space, for every point, the filter of its neighborhoods has a basis composed of closed sets.
`eq_of_nhds_neBot` theorem eq_of_nhds_neBot : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {x y : X}, (nhds x ⊓ nhds y).NeBot → x = y := by sorry This theorem states that for any type `X` equipped with a topology (i.e., `X` is a topological space) and satisfying the Hausdorff condition (also known as a `T2Space`), given any two elements `x` and `y` from `X`, if the intersection of the neighborhood filters of `x` and `y` is not the bottom filter (i.e., it is not empty), then `x` must be equal to `y`. This theorem captures a key property of Hausdorff spaces: distinct points have disjoint neighborhoods. More concisely: In a Hausdorff topological space, distinct points have disjoint neighborhoods, i.e., if `x` and `y` are distinct points and their neighborhood filters intersect non-emptily, then `x = y`.
`IsCompact.isCompact_isClosed_basis_nhds` theorem IsCompact.isCompact_isClosed_basis_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {x : X} {L : Set X}, IsCompact L → L ∈ nhds x → (nhds x).HasBasis (fun K => K ∈ nhds x ∧ IsCompact K ∧ IsClosed K) fun x => x This theorem states that for any point in an R₁ space, if it has a compact neighborhood, then it has a basis of compact closed neighborhoods. Here, an R₁ space is a type of topological space with certain properties. The theorem takes as input a topological space `X`, a point `x` in `X`, and a set `L` in `X`. If `L` is a compact set and a neighborhood of `x`, then the neighborhood filter at `x` has a basis consisting of sets that are also neighborhoods of `x`, and are additionally both compact and closed. A basis of a filter is a collection of sets that suffice to generate the filter by taking intersections and supersets. This theorem plays a significant role in the study of the topological properties of points and sets within a space. More concisely: In an R₁ space, if a point has a compact neighborhood, then it has a basis of compact and closed neighborhoods.
`nhdsWithin_of_mem_discrete` theorem nhdsWithin_of_mem_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [inst_1 : DiscreteTopology ↑s] {x : X}, x ∈ s → nhdsWithin x s = pure x The theorem `nhdsWithin_of_mem_discrete` says the following: Given any type `X` equipped with a topological space structure, a set `s` of `X`, and an element `x` of `X`, if the set `s` has a discrete topology, and `x` is an element of `s`, then the neighborhood filter of `x` within `s` is equal to the pure `x` filter. The pure `x` filter is the principal filter at the singleton `{x}`. In simpler terms, in a discrete topological space, the set of all neighborhoods of `x` within `s` collapses to just `{x}` when `x` is in `s`. More concisely: In a discrete topological space, the neighborhood filter of an element in the set is equal to its principal filter.
`Embedding.t2Space` theorem Embedding.t2Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y] {f : X → Y}, Embedding f → T2Space X This theorem states that if you have a topological embedding from a type `X` to a type `Y`, and if the topological space `Y` is a Hausdorff space (also known as a T2 space), then the topological space `X` is also a Hausdorff space. Topological embedding is a function which preserves the topology, and a Hausdorff space is a topological space where any two distinct points have disjoint open neighborhoods. This theorem shows the preservation of the Hausdorff property under topological embeddings. More concisely: If `X` is a topological space embedded as a subspace of the Hausdorff space `Y`, then `X` is also a Hausdorff space.
`RegularSpace.ofBasis` theorem RegularSpace.ofBasis : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : X → Sort u_3} {p : (a : X) → ι a → Prop} {s : (a : X) → ι a → Set X}, (∀ (a : X), (nhds a).HasBasis (p a) (s a)) → (∀ (a : X) (i : ι a), p a i → IsClosed (s a i)) → RegularSpace X The theorem `RegularSpace.ofBasis` states that for any type `X` with a topological space structure, given a family of sets `s` indexed by some function `ι` and some property `p`, if every neighborhood filter at a point `a` in `X` has a basis specified by `p` and `s`, and for every `a` in `X` and index `i` of type `ι a`, if `p a i` holds then the corresponding set `s a i` is closed, then `X` is a regular space. In other words, this theorem provides a criterion for a topological space to be a regular space based on the existence of a certain basis for every neighborhood filter and the closure of the sets in this basis. More concisely: A topological space `X` is regular if every neighborhood filter at each point `a` in `X` has a basis specified by property `p` on indexed family `s`, and all sets `s a i` are closed whenever `p a i` holds.
`SeparatedNhds.symm` theorem SeparatedNhds.symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → SeparatedNhds t s This theorem, named `SeparatedNhds.symm`, states that for any type `X` that has a topological space structure and any two subsets `s` and `t` of `X`, if `s` and `t` satisfy the `SeparatedNhds` predicate (i.e., there exist disjoint open sets `U` and `V` such that `s` is a subset of `U` and `t` is a subset of `V`), then `t` and `s` also satisfy the `SeparatedNhds` predicate. Essentially, it asserts that the `SeparatedNhds` property is symmetric: if `s` and `t` are separated by neighbourhoods, then so are `t` and `s`. More concisely: If subsets `s` and `t` of a topological space `X` are separated (i.e., there exist disjoint open sets containing each), then `s` and `t` are symmetrically separated.
`infinite_of_mem_nhds` theorem infinite_of_mem_nhds : ∀ {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : T1Space X] (x : X) [hx : (nhdsWithin x {x}ᶜ).NeBot] {s : Set X}, s ∈ nhds x → s.Infinite This theorem states that for any topological space `X` that is also a `T1` space (a topological space where for any pair of distinct points, each has a neighborhood not containing the other), given a point `x` in `X` such that the punctured neighborhoods of `x` form a nontrivial filter (the filter of neighborhoods of `x` excluding `x` is not the bottom filter), any neighborhood `s` of `x` is infinite. In other words, if `s` is a neighborhood of `x` (meaning it contains an open set around `x`), then `s` has infinitely many elements. This theorem highlights a property of the local structure of `T1` spaces: if we remove a single point from the neighborhoods, the remaining sets in the filter are still large enough (infinite) to form a nontrivial filter. More concisely: In any T1 topological space, if a point has a nontrivial filter of punctured neighborhoods, then each neighborhood of that point contains an infinite number of elements.
`isOpen_singleton_of_finite_mem_nhds` theorem isOpen_singleton_of_finite_mem_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] (x : X) {s : Set X}, s ∈ nhds x → s.Finite → IsOpen {x} The theorem `isOpen_singleton_of_finite_mem_nhds` states that for any given point `x` in a topological space `X` with a T1 space property, if there exists a set `s` in the neighborhood of `x` and this set `s` is finite, then the singleton set containing only the point `x` is an open set in the topological space `X`. In other words, if around a point we can find a finite neighborhood, the point must be isolated, i.e., it forms an open set by itself within the context of the topological space `X`. This condition is only true in topological spaces that satisfy the T1 axiom (every singleton set is closed). More concisely: In a T1 topological space, if a point has a finite neighborhood, then the singleton set containing that point is open.
`Mathlib.Topology.Separation._auxLemma.4` theorem Mathlib.Topology.Separation._auxLemma.4 : ∀ {a b : Prop}, (a ∧ b) = (b ∧ a) This theorem, located in the Topology.Separation module of the Mathlib library, is stating that for any two propositions 'a' and 'b', the conjunction 'a and b' is equivalent to 'b and a'. In other words, the order in which the propositions are presented in an 'and' statement does not affect the truth of the statement; this is a fundamental property of logical conjunctions. More concisely: For all propositions 'a' and 'b', the conjunction 'a ∧ b' is equivalent to 'b ∧ a'.
`Specializes.inseparable` theorem Specializes.inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R0Space X] {x y : X}, x ⤳ y → Inseparable x y In a topological space that satisfies the R0 separation axiom (also known as an R0 space), if one point specializes to another (denoted as `x ⤳ y`), then these two points are inseparable. In other words, for any two points `x` and `y` in such an R0 space, if every open set containing `y` also contains `x`, then the neighborhoods of `x` and `y` are identical, which is the definition of `x` and `y` being inseparable. More concisely: In an R0 topological space, if one point specializes to another, then they are inseparable.
`IsCompact.closure_of_subset` theorem IsCompact.closure_of_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {s K : Set X}, IsCompact K → s ⊆ K → IsCompact (closure s) This theorem states that in any topological space, if a set `K` is compact and `s` is a subset of `K`, then the closure of `s` is also compact. Here, compactness refers to the property that for any nontrivial filter containing the set, there is a point in the set such that every set in the filter intersects every neighborhood of that point. The closure of a set is the smallest closed set that contains it. More concisely: In any topological space, if a compact set `K` contains a subset `s`, then the closure of `s` is also compact.
`Set.EqOn.closure` theorem Set.EqOn.closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space X] {s : Set Y} {f g : Y → X}, Set.EqOn f g s → Continuous f → Continuous g → Set.EqOn f g (closure s) This theorem states that if two continuous functions `f` and `g` (mapping from a set `Y` to a topological space `X`) are equal on a set `s`, then they are also equal on the closure of `s`. The closure of `s` is defined as the smallest closed set that contains `s`. This theorem applies under the condition that the topological space `X` is also a T2 space (also known as a Hausdorff space), which is a topological property that guarantees a certain level of separability of points. The theorem allows the extension of equality from a set to its closure, given that the involved functions are continuous. More concisely: If `f` and `g` are continuous functions from a set `Y` to a T2 topological space `X` and `f(y) = g(y)` for all `y` in a set `s`, then `f(y) = g(y)` for all `y` in the closure of `s`.
`exists_subset_nhds_of_isCompact` theorem exists_subset_nhds_of_isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {ι : Type u_4} [inst_2 : Nonempty ι] {V : ι → Set X}, Directed (fun x x_1 => x ⊇ x_1) V → (∀ (i : ι), IsCompact (V i)) → ∀ {U : Set X}, (∀ x ∈ ⋂ i, V i, U ∈ nhds x) → ∃ i, V i ⊆ U The theorem `exists_subset_nhds_of_isCompact` asserts the following: Given a topological space `X` that is also a Hausdorff (or T2) space and a nonempty index set `ι`, if we have a decreasing family of compact sets `V : ι → Set X` (meaning for any two indices in the set `ι`, there exists another index such that the corresponding set includes the sets corresponding to the initial two indices), then for any set `U` that is a neighborhood of the intersection of all the sets in the family `V`, there exists an index `i` such that the set `V i` is contained within `U`. This occurs without having to assume each `V i` is closed because it follows from the compactness of the family of sets `V` and the Hausdorff property of the space `X`. More concisely: In a Hausdorff topological space, if if there is a decreasing family of compact sets, then for any neighborhood of their intersection, there exists a set in the family contained within it.
`IsCompact.mem_closure_iff_exists_inseparable` theorem IsCompact.mem_closure_iff_exists_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {y : X} {K : Set X}, IsCompact K → (y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y) The theorem states that in a R₁ space (a type of topological space), given a compact set `K`, a point `y` belongs to the closure of `K` if and only if there exists at least one point `x` in `K` from which `y` is inseparable topologically. In other words, the neighborhoods of `y` and `x` are identical, which means every open set that contains `y` also contains `x` and vice versa. More concisely: In a R₁ space, a point belongs to the closure of a compact set if and only if there exists a point in the set with which it is topologically inseparable.
`specializes_iff_eq` theorem specializes_iff_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] {x y : X}, x ⤳ y ↔ x = y This theorem, called "specializes_iff_eq", states that for any type `X` equipped with a topological space structure and a T1 space structure, and for any two elements `x` and `y` of `X`, the statement "`x` specializes `y`" is equivalent to "`x` equals `y`". Here, "specializes" is a concept in topology which, in a T1 space, turns out to be equivalent to equality. This theorem thus connects an abstract topological concept to a more intuitive, everyday concept of equality. More concisely: In a T1 topological space, an element specializes another if and only if they are equal.
`exists_open_superset_and_isCompact_closure` theorem exists_open_superset_and_isCompact_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] [inst_2 : WeaklyLocallyCompactSpace X] {K : Set X}, IsCompact K → ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V) This theorem states that in a weakly locally compact space that also obeys the R₁ space condition, every compact set has an open neighborhood whose closure is also compact. To be specific, given any type `X` with a topological space structure, an R₁ Space structure, and a weakly locally compact space structure, for any set `K` of `X` that is compact, there exists a set `V` such that `V` is open, `K` is a subset of `V`, and the closure of `V` is compact. More concisely: In a weakly locally compact and R₁ space, every compact set has an open neighborhood with compact closure.
`Mathlib.Topology.Separation._auxLemma.65` theorem Mathlib.Topology.Separation._auxLemma.65 : ∀ {X : Type u_3} [inst : TopologicalSpace X], R1Space X = ∀ (x y : X), Inseparable x y ∨ Disjoint (nhds x) (nhds y) This theorem states that for any type `X` which is equipped with a topology, `X` is an R1 space if and only if for any two points `x` and `y` in `X`, either `x` and `y` are inseparable (i.e., for every open set `s`, `x` is in `s` if and only if `y` is in `s`) or the neighborhoods of `x` and `y` (represented by the filters `nhds x` and `nhds y`) are disjoint (meaning that there is no common smaller neighborhood of `x` and `y`, formally, their infimum is the bottom element). More concisely: A topological space X, equipped with a topology, is an R1 space if and only if for all points x and y in X, their neighborhood filters are either identical or have empty infimum.
`Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete` theorem Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_3} {p : ι → Prop} {t : ι → Set X} {s : Set X} [inst_1 : DiscreteTopology ↑s] {x : X}, (nhds x).HasBasis p t → x ∈ s → ∃ i, p i ∧ t i ∩ s = {x} This theorem states that for any type `X` equipped with a topological space structure, another type `ι`, a property `p` defined on `ι`, and a function `t` from `ι` to sets of `X`, given a set `s` of `X` with a discrete topology, and an element `x` of `X`, if the neighborhood filter at `x` has a basis indexed by `ι` with properties `p` and corresponding sets `t`, and `x` is an element of `s`, then there exists an index `i` such that the property `p` holds for `i`, and the intersection of the set `t(i)` and `s` is the singleton set containing `x`. In simpler terms, if you have a point `x` in a discrete set `s` in a topological space, and you know the basis of the neighborhoods around `x`, then you can find a basis element such that it intersects `s` exactly at `x`. More concisely: For any discrete set $s \subseteq X$ in a topological space, and any point $x \in s$ with a neighborhood basis indexed by $\iota$ satisfying property $p$ and having sets $t(\iota)$, there exists an index $\iota_0$ such that $x \in t(\iota_0) \cap s$ is a singleton.
`compact_t2_tot_disc_iff_tot_sep` theorem compact_t2_tot_disc_iff_tot_sep : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : CompactSpace X], TotallyDisconnectedSpace X ↔ TotallySeparatedSpace X This theorem, `compact_t2_tot_disc_iff_tot_sep`, states that for any type `X` which has a topological space structure, a T2 space structure (also known as a Hausdorff space), and a compact space structure, `X` is a totally disconnected space if and only if it is a totally separated space. This is also true for locally compact spaces. In mathematical terms, a compact Hausdorff space is totally disconnected (i.e., its only connected subspaces are one-point sets) if and only if it is totally separated (i.e., for any two distinct points, there exists a separation of the space into two open sets, one containing the first point and the other containing the second). More concisely: A compact Hausdorff space (resp. locally compact Hausdorff space) is totally disconnected if and only if it is totally separated.
`Specializes.eq` theorem Specializes.eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] {x y : X}, x ⤳ y → x = y This theorem, referred to as `Specializes.eq`, states that for any type `X` which is a topological space and additionally has the `T1` property (every singleton set is closed), if a point `x` specializes to a point `y` (notation `x ⤳ y`, meaning that every neighborhood of `x` is also a neighborhood of `y`), then `x` must be equal to `y`. This theorem essentially states that in `T1` spaces, the specialization relation is trivial: a point specializes to another if and only if they are the same. More concisely: In a T1 topological space `X`, if `x` specializes to `y` (`x ⤳ y`), then `x` equals `y`.
`t2_iff_nhds` theorem t2_iff_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X], T2Space X ↔ ∀ {x y : X}, (nhds x ⊓ nhds y).NeBot → x = y This theorem states that a topological space is T2 (also known as a Hausdorff space) if and only if the intersection of the neighborhood filters of any two distinct points cannot generate the bottom filter. In other words, given any two distinct points in a T2 space, there exists a neighborhood for each point such that these neighborhoods do not overlap. This captures the property that in a T2 space, distinct points can be separated by open neighborhoods. More concisely: A topological space is T2 (Hausdorff) if and only if the neighborhood filters of any two distinct points have empty intersection.
`exists_isOpen_superset_and_isCompact_closure` theorem exists_isOpen_superset_and_isCompact_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] [inst_2 : WeaklyLocallyCompactSpace X] {K : Set X}, IsCompact K → ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V) This theorem states that in a weakly locally compact Hausdorff space, every compact set has an open neighborhood whose closure is compact. More precisely, for any type `X` with a topological space structure, R₁ space structure, and weakly locally compact space structure, and any compact set `K` of `X`, there exists an open set `V` such that `K` is a subset of `V` and the closure of `V` is compact. More concisely: In a weakly locally compact Hausdorff space, every compact set has an open neighborhood with compact closure.
`compact_exists_isClopen_in_isOpen` theorem compact_exists_isClopen_in_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : CompactSpace X] [inst_3 : TotallyDisconnectedSpace X] {x : X} {U : Set X}, IsOpen U → x ∈ U → ∃ V, IsClopen V ∧ x ∈ V ∧ V ⊆ U The theorem, `compact_exists_isClopen_in_isOpen`, states that for any type `X` which has a topological space structure, is a T2 space (also known as a Hausdorff space), is a compact space and is a totally disconnected space, for any element `x` of `X` and any set `U` of `X` that is open, if `x` is an element of `U`, then there exists a set `V` such that `V` is both closed and open (also known as a clopen set), `x` is an element of `V`, and `V` is a subset of `U`. In other words, in a compact, Hausdorff, totally disconnected topological space, every member of an open set is contained in a clopen subset of the open set. More concisely: In a compact, Hausdorff, and totally disconnected topological space, every open set contains a clopen subset that includes any given point in the set.
`exists_isOpen_mem_isCompact_closure` theorem exists_isOpen_mem_isCompact_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] [inst_2 : WeaklyLocallyCompactSpace X] (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U) This theorem states that in a weakly locally compact R₁ space, every point possesses an open neighborhood with a compact closure. In more specific terms, for any type `X` that is a topological space, a R₁ space, and a weakly locally compact space, every element `x` of `X` has an open set `U` such that `x` belongs to `U` and the closure of `U`, which is the smallest closed set containing `U`, is compact. Compactness here means that for any nontrivial filter `f` containing the set, there exists a point in the set where every set of the filter intersects every neighborhood of that point. More concisely: In a weakly locally compact R₁ space, every point has an open neighborhood with a compact closure.
`separated_by_continuous` theorem separated_by_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y] {f : X → Y}, Continuous f → ∀ {x y : X}, f x ≠ f y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v This theorem, `separated_by_continuous`, states that for any two types `X` and `Y` with `X` and `Y` being topological spaces and `Y` being a `T2Space` (also known as a Hausdorff space), if there exists a continuous function `f` from `X` to `Y`, then for any two distinct elements `x` and `y` in `X` (i.e., `f(x)` and `f(y)` are not equal), there exist two open sets `u` and `v` such that `x` is in `u`, `y` is in `v`, and `u` and `v` are disjoint. This is essentially a formulation of the separation axiom in topology that in a Hausdorff space, distinct points can be separated by open neighborhoods. More concisely: In a Hausdorff space, for any two distinct points, there exist disjoint open sets containing each point.
`Set.EqOn.of_subset_closure` theorem Set.EqOn.of_subset_closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y] {s t : Set X} {f g : X → Y}, Set.EqOn f g s → ContinuousOn f t → ContinuousOn g t → s ⊆ t → t ⊆ closure s → Set.EqOn f g t The theorem, `Set.EqOn.of_subset_closure`, states that for a given pair of functions `f` and `g` mapping from a topological space `X` to a `T2` space `Y`, if `f` and `g` are equal on a subset `s` and both functions are continuous on a subset `t` such that `s` is a subset of `t` and `t` is a subset of the closure of `s`, then `f` and `g` are also equal on the subset `t`. This theorem is related to the concept of closure in topology and function equality on sets. More concisely: If `f` and `g` are continuous functions mapping a topological space `X` to a T2 space `Y`, `f(s) = g(s)` for all `s` in a subset `s` of `X`, `s` is a subset of `t`, and `t` is a subset of the closure of `s`, then `f(t) = g(t)`.
`Mathlib.Topology.Separation._auxLemma.8` theorem Mathlib.Topology.Separation._auxLemma.8 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t = Disjoint (nhdsSet s) (nhdsSet t) This theorem states that for any topological space 'X' and any two subsets 's' and 't' of 'X', the two subsets are SeparatedNhds (i.e., they can be separated by two disjoint open sets in the topological space) if and only if the filters of neighborhoods of the two subsets are Disjoint (i.e., their meet is the bottom element of the lattice of filters). Thus, it gives a condition for the separation of two sets in terms of the disjointness of their neighborhood filters in the topological space. More concisely: Two subsets of a topological space are separated if and only if their filters of neighborhoods are disjoint.
`isCompact_closure_of_subset_compact` theorem isCompact_closure_of_subset_compact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {s K : Set X}, IsCompact K → s ⊆ K → IsCompact (closure s) This theorem states that for any topological space `X` with an R1 space structure (every pair of distinct points in `X` has disjoint neighborhoods), if `K` is a compact set and `s` is a subset of `K`, then the closure of `s` is also compact. In other words, the closure of any subset of a compact set in such a space is itself compact. It underscores a fundamental property of compact sets in topological spaces: compactness is preserved under closure operations. More concisely: In a topological space with the R1 property, the closure of any compact subset is compact.
`Specializes.symm` theorem Specializes.symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R0Space X] {x y : X}, x ⤳ y → y ⤳ x This theorem states that in a topological space X, which also satisfies the R0 separation axiom (R0Space), the 'Specializes' relation is symmetric when applied to any two points x and y in the space X. This means that if x specializes to y, then y also specializes to x. The 'Specializes' relation is a concept in topology that signifies that every neighbourhood of x also contains y. More concisely: In a topological space X satisfying R0 separation axiom, the 'Specializes' relation is symmetric: if x specializes to y, then y specializes to x.
`t2_iff_isClosed_diagonal` theorem t2_iff_isClosed_diagonal : ∀ {X : Type u_1} [inst : TopologicalSpace X], T2Space X ↔ IsClosed (Set.diagonal X) The theorem `t2_iff_isClosed_diagonal` states that for any type `X` equipped with a topology (given by the instance `TopologicalSpace X`), `X` is a T2 space if and only if the diagonal set of `X` (which contains all pairs of the form `(a, a)`) is a closed set in the product topology on `X × X`. Here, a T2 space or Hausdorff space is a topological space in which distinct points have disjoint neighborhoods. More concisely: A topological space X equipped with a topology is a T2 space if and only if the diagonal set in X × X is a closed set in the product topology.
`Continuous.isClosedMap` theorem Continuous.isClosedMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : CompactSpace X] [inst_3 : T2Space Y] {f : X → Y}, Continuous f → IsClosedMap f The theorem states that a continuous map from a compact space to a Hausdorff space is a closed map. In other words, for any types `X` and `Y` with topological space structures, if `X` is compact, `Y` is a Hausdorff space, and `f` is a continuous function from `X` to `Y`, then `f` is a closed map. A closed map being a function such that the image of any closed set in `X` is also closed in `Y`. More concisely: A continuous function from a compact space to a Hausdorff space is a closed map.
`Inducing.embedding` theorem Inducing.embedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T0Space X] {f : X → Y}, Inducing f → Embedding f This theorem states that for any two types `X` and `Y`, given that `X` is a T₀ space (a topological space with a Kolmogorov property, where for any two distinct points there exists a neighborhood of one that does not contain the other), and `f` is a function from `X` to `Y` that induces the topology of `Y`, then `f` is a topological embedding. In other words, a function that induces the topology from a T₀ space is guaranteed to be an embedding, preserving the topological properties of the space. More concisely: If `X` is a T₀ space and `f : X → Y` induces the topology of `Y`, then `f` is a topological embedding from `X` to `Y`.
`T2Space.of_injective_continuous` theorem T2Space.of_injective_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y] {f : X → Y}, Function.Injective f → Continuous f → T2Space X The theorem `T2Space.of_injective_continuous` states that if we have an injective continuous function from a space 'X' to a space 'Y', and 'Y' is a Hausdorff space (T2 space), then 'X' is also a Hausdorff space. A Hausdorff space is a topological space in which distinct points have disjoint neighborhoods, an injective function is one where different inputs always produce different outputs, and a continuous function is one that does not have jumps or breaks. More concisely: If a continuous, injective function maps a Hausdorff space to another Hausdorff space, then the domain space is Hausdorff.
`Mathlib.Topology.Separation._auxLemma.5` theorem Mathlib.Topology.Separation._auxLemma.5 : ∀ {a b c : Prop}, (a ∧ b ∧ c) = (b ∧ a ∧ c) This theorem states that for any three propositions `a`, `b`, and `c`, the statement that `a` and `b` and `c` are all true is equivalent to the statement that `b` and `a` and `c` are all true. In other words, the order in which we consider the conjunction of propositions does not matter. More concisely: The theorem asserts that for any propositions `a`, `b`, and `c`, the conjunctions `a ∧ b ∧ c` and `b ∧ a ∧ c` are logically equivalent.
`NormalSpace.normal` theorem NormalSpace.normal : ∀ {X : Type u} [inst : TopologicalSpace X] [self : NormalSpace X] (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t The theorem `NormalSpace.normal` states that in a normal topological space, given any two disjoint closed sets, there exist two neighbourhoods of these sets that are also disjoint. In other words, for any topological space that satisfies the condition of being a normal space, and for any two closed sets in this space that do not share any common elements, it is always possible to find two open sets (neighbourhoods), each containing one of the closed sets, which also do not have any common elements. This theorem is a key property of normal spaces in topology. More concisely: In a normal topological space, for any two disjoint closed sets, there exist disjoint open neighborhoods.
`Continuous.ext_on` theorem Continuous.ext_on : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space X] {s : Set Y}, Dense s → ∀ {f g : Y → X}, Continuous f → Continuous g → Set.EqOn f g s → f = g This theorem states that if there are two continuous functions `f` and `g` from a topological space `Y` to another topological space `X`, which is also a T2 space (or Hausdorff space), and if these two functions are equal on a dense set `s` in `Y`, then the two functions `f` and `g` are equal everywhere. In other words, if `f` and `g` agree on all points in a set `s` that is dense in `Y`, then `f` and `g` must be the same function. More concisely: If `f` and `g` are continuous functions from a dense subset `s` of a T2 space `Y` to a topological space `X`, and `f(y) = g(y)` for all `y` in `s`, then `f = g`.
`isClosed_singleton` theorem isClosed_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] {x : X}, IsClosed {x} This theorem states that for any given type `X` with an instance of a topological space and a T1 space, any singleton set which contains a single element `x` of type `X` is a closed set. In other words, in a T1 topological space, singletons are always closed sets. More concisely: In a T1 topological space, the singleton set of any point is a closed set.
`disjoint_nhds_nhds` theorem disjoint_nhds_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {x y : X}, Disjoint (nhds x) (nhds y) ↔ x ≠ y This theorem states that for any topological space `X` which also satisfies the T2 separation axiom (also known as a Hausdorff space), two points `x` and `y` in `X` have disjoint neighborhood filters (i.e., there are no elements common to both filters) if and only if `x` is not equal to `y`. The T2 separation axiom guarantees that for any two distinct points in the space, there exist non-overlapping open neighborhoods around each point. Hence, the theorem essentially formalizes the notion that distinct points in a Hausdorff space have distinct neighborhood filters. More concisely: In a T2 topological space, two distinct points have disjoint neighborhood filters.
`Mathlib.Topology.Separation._auxLemma.3` theorem Mathlib.Topology.Separation._auxLemma.3 : ∀ {a b c : Prop}, ((a ∧ b) ∧ c) = (a ∧ b ∧ c) This theorem states that for any three propositions `a`, `b`, and `c`, the logical conjunction of `a` and `b`, further conjoined with `c` (i.e., `(a ∧ b) ∧ c`), is logically equivalent to the conjunction of `a`, `b`, and `c` without any specific grouping (i.e., `a ∧ b ∧ c`). This essentially means that the association of conjunctions (and-operators) does not alter the truth value of the overall expression. More concisely: The theorem asserts that for all propositions `a`, `b`, and `c`, the logical expressions `(a ∧ b) ∧ c` and `a ∧ b ∧ c` are logically equivalent.
`T0Space.t0` theorem T0Space.t0 : ∀ {X : Type u} [inst : TopologicalSpace X] [self : T0Space X] ⦃x y : X⦄, Inseparable x y → x = y The theorem `T0Space.t0` states that in a T₀ space (a topological space with the property that for any two distinct points there exists a neighborhood of one that does not contain the other), two inseparable points are necessarily equal. In other words, if in a T₀ space, two points `x` and `y` are such that the neighborhood of `x` is the same as the neighborhood of `y`, then `x` and `y` must be the same point. The definition of inseparable points used here is that the neighborhoods of the two points are the same (`nhds x = nhds y`). More concisely: In a T₀ space, two inseparable points are equal. (Two points `x` and `y` are inseparable if and only if their neighborhoods are equal: `nhds x = nhds y` implies `x = y`.)
`t2Space_iff_disjoint_nhds` theorem t2Space_iff_disjoint_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X], T2Space X ↔ Pairwise fun x y => Disjoint (nhds x) (nhds y) This theorem states that for any type `X` equipped with a topological structure, `X` is a T2-space (also known as a Hausdorff space) if and only if for every pair of distinct elements `x` and `y` in `X`, the neighborhoods of `x` and `y` are disjoint. In mathematical terms, the neighborhoods are disjoint if their intersection is the bottom element, symbolically represented as `⊥`. Here, 'disjoint' is generalized from the notion of disjoint sets to elements of a lattice by defining two elements as disjoint if their infimum (greatest lower bound) is the bottom element. More concisely: A topological space `X` is T2 (Hausdorff) if and only if for all distinct points `x` and `y` in `X`, the neighborhood filters of `x` and `y` have empty intersection (i.e., their infimum is the bottom element).
`Dense.diff_finite` theorem Dense.diff_finite : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] [inst_2 : ∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X}, Dense s → ∀ {t : Set X}, t.Finite → Dense (s \ t) This theorem states that for any topological space `X` which does not have isolated points, and any dense set `s` in this space, if we remove a finite set `t` from `s`, the resulting set remains dense. In formal terms, if `X` is a topological space without isolated points and `s` is a dense set in `X`, then for any finite set `t`, the difference set `s \ t` is still dense in `X`. This means that even after removing a finite number of points from a dense set in such a space, every point in the space is either in the resultant set or is a limit point of the resultant set. More concisely: In a topological space without isolated points, any finite subset of a dense set leaves behind a still dense residual set.
`IsCompact.closure_eq_biUnion_closure_singleton` theorem IsCompact.closure_eq_biUnion_closure_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {K : Set X}, IsCompact K → closure K = ⋃ x ∈ K, closure {x} In a Hausdorff space, also known as an R₁ space, the theorem `IsCompact.closure_eq_biUnion_closure_singleton` states that for any compact set `K`, the closure of `K` is equal to the union of the closures of its singleton points. In other words, the smallest closed set containing the compact set `K` is the union of the smallest closed sets containing each point `x` in `K`. This theorem holds for any type `X` that has a topology and satisfies the R₁ space condition, which generally requires that any two distinct points in the space can be separated by disjoint open neighbourhoods. More concisely: In a Hausdorff space, the closure of a compact set is equal to the union of the closures of its singleton points.
`QuotientMap.of_surjective_continuous` theorem QuotientMap.of_surjective_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : CompactSpace X] [inst_3 : T2Space Y] {f : X → Y}, Function.Surjective f → Continuous f → QuotientMap f The theorem `QuotientMap.of_surjective_continuous` states that for any types `X` and `Y` equipped with topological spaces, where `X` is compact and `Y` is a Hausdorff space, a function `f` from `X` to `Y` is a quotient map if it is both surjective and continuous. In more mathematical terms, if `f: X → Y` is a continuous, surjective function from a compact space `X` to a Hausdorff space `Y`, then `f` is a quotient map, meaning that for all sets `s` in `Y`, `s` is an open set if and only if its preimage under `f` is an open set in `X`. More concisely: If `f: X → Y` is a continuous, surjective function from a compact space `X` to a Hausdorff space `Y`, then `f` is a quotient map.
`Filter.Tendsto.limUnder_eq` theorem Filter.Tendsto.limUnder_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : T2Space X] {x : X} {f : Filter Y} [inst_2 : f.NeBot] {g : Y → X}, Filter.Tendsto g f (nhds x) → limUnder f g = x This theorem establishes an equivalence between the notion of a limit and the concept of a function tending towards a limit in a topological space. Specifically, for any topological space `X` that is also a `T2Space` (a space in which any two distinct points have disjoint open neighborhoods), given any point `x` in `X` and a filter `f` on an arbitrary type `Y` (where the filter is not the smallest filter, i.e., not the bottom element), and a function `g` from `Y` to `X`. If the function `g` tends towards the neighborhood filter of `x` under the filter `f` (i.e., for every neighborhood of `x`, there is a set in filter `f` such that the image of that set under `g` falls inside the neighborhood), then the limit of the function `g` under the filter `f` is `x`. This theorem essentially asserts that under these conditions, the limit is unique and is equal to the point towards which the function tends. More concisely: In a T2 topological space, if a function tends towards a point under a non-bottom filter, then the limit of the function under that filter equals the point.
`Dense.diff_singleton` theorem Dense.diff_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] {s : Set X}, Dense s → ∀ (x : X) [inst_2 : (nhdsWithin x {x}ᶜ).NeBot], Dense (s \ {x}) The theorem `Dense.diff_singleton` states that for any topological space `X` with the T1 separation axiom (T1Space), and any set `s` in `X` that is dense, when we remove a non-isolated point `x` from `s` (i.e., a point `x` for which the neighborhood within the set of points not equal to `x` is non-empty), the resulting set `s \ {x}` (set `s` minus singleton `{x}`) is still dense. In other words, removing a non-isolated point from a dense set in a T1 topological space does not affect the density of the set. More concisely: In a T1 topological space, removing a non-isolated point from a dense set results in a still dense set.
`Dense.diff_finset` theorem Dense.diff_finset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] [inst_2 : ∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X}, Dense s → ∀ (t : Finset X), Dense (s \ ↑t) This theorem states that for any given topological space `X` that does not have isolated points, if we have a set `s` that is dense in this space, then removing any finite set `t` from `s` still results in a dense set. Here, a set is considered dense if every point in the space belongs to its closure, and a space is said to have no isolated points if the neighborhood of any point `x` that excludes `x` itself is not a trivial neighborhood. In other words, the removal of any finite number of points from a dense set in such a space does not affect its density. More concisely: In a Hausdorff topological space without isolated points, a dense set remains dense after removing any finite number of points.
`IsCompact.closure` theorem IsCompact.closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {K : Set X}, IsCompact K → IsCompact (closure K) The theorem `IsCompact.closure` states that, given any type `X` equipped with a topology and an R1 space structure, and any set `K` of type `X`, if `K` is a compact set then the closure of `K` is also a compact set. In other words, if every nontrivial filter that contains `K` has a cluster point in `K`, then the same property holds for the smallest closed set containing `K`. This theorem is typically applicable in the context of topological and metric spaces. More concisely: If `K` is a compact subset of a topological space `X` with an R1 structure, then the closure of `K` is also a compact subset of `X`.
`t2_separation` theorem t2_separation : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {x y : X}, x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v The theorem `t2_separation` states that in any T2 space (also known as a Hausdorff space), for any two distinct points, there exist two open sets such that each point belongs to one of the open sets and the open sets are disjoint. This means, in the context of topology, that given the points `x` and `y` are different, there are open sets `u` and `v` where `x` is in `u`, `y` is in `v`, and there is no overlap between `u` and `v`. The disjointness of the sets is defined in general lattice terms, i.e., their infimum (greatest lower bound) is the bottom element. More concisely: In a T2 space, given any two distinct points, there exist open sets containing each point that are disjoint, i.e., have an empty intersection.
`IsCompact.closure_eq_biUnion_inseparable` theorem IsCompact.closure_eq_biUnion_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {K : Set X}, IsCompact K → closure K = ⋃ x ∈ K, {y \| Inseparable x y} This theorem states that for any compact set `K` in a classical (T1) topological space `X`, the closure of `K` is equal to the union of all inseparable sets `{y \| Inseparable x y}` for each `x` in `K`. In other words, the smallest closed set containing `K` is the union of all sets of points that are topologically inseparable from each point in `K`. Here, two points are called inseparable if they have the same neighborhoods. More concisely: The closure of a compact set in a T1 topological space is equal to the union of all inseparable sets with respect to each point in the set.
`IsCompact.finite_compact_cover` theorem IsCompact.finite_compact_cover : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {s : Set X}, IsCompact s → ∀ {ι : Type u_3} (t : Finset ι) (U : ι → Set X), (∀ i ∈ t, IsOpen (U i)) → s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i The theorem states that for a given compact set in a topological space with a R1 space structure, and an indexed family of open sets that covers this compact set, there exists another indexed family of compact sets, each of which is a subset of the corresponding open set in the family, such that the union of these compact sets is equal to the original compact set. In other words, any finite open cover of a compact set contains a finite compact cover of the same set. More concisely: Given a compact set in a T1 topological space and a finite open cover, there exists a finite compact cover.
`separatedNhds_of_isCompact_isCompact` theorem separatedNhds_of_isCompact_isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {s t : Set X}, IsCompact s → IsCompact t → Disjoint s t → SeparatedNhds s t This theorem, which is an alias of `SeparatedNhds.of_isCompact_isCompact`, states that in a topological space that is also a T2 space (a space in which any two distinct points have disjoint neighborhoods), for any two compact sets that are disjoint, they are also separated. In other words, there exist open sets which contain these two compact sets respectively, and these two open sets are disjoint. Compactness here means that for any nontrivial filter that contains the set, there exists a point in the set such that every set of the filter meets every neighborhood of this point. Two sets are disjoint if their infimum is the bottom element. Two sets are separated if they can be covered by two disjoint open sets. More concisely: In a T2 topological space, any two disjoint compact sets are separated by disjoint open sets.
`exists_compact_closed_between` theorem exists_compact_closed_between : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LocallyCompactSpace X] [inst_2 : RegularSpace X] {K U : Set X}, IsCompact K → IsOpen U → K ⊆ U → ∃ L, IsCompact L ∧ IsClosed L ∧ K ⊆ interior L ∧ L ⊆ U This theorem states that in a locally compact regular space (which may not be Hausdorff), for any given containment of a compact set `K` within an open set `U`, there exists a compact closed set `L` such that `K` is a subset of the interior of `L` and `L` is a subset of `U`. In other words, the compact closed set `L` is a "neighborhood" that lies between the compact set `K` and the open set `U`. More concisely: In a locally compact regular space, for any compact subset `K` of an open set `U`, there exists a compact closed set `L` containing `K` with `L` being a subset of the interior of `U`.
`RegularSpace.regular` theorem RegularSpace.regular : ∀ {X : Type u} [inst : TopologicalSpace X] [self : RegularSpace X] {s : Set X} {a : X}, IsClosed s → a ∉ s → Disjoint (nhdsSet s) (nhds a) This theorem states that if `a` is a point that does not belong to a closed set `s` in a topological space `X` that is a regular space, then there exist disjoint neighborhoods for `a` and `s`. In other words, you can find a neighborhood (a set that contains an open set) around the point `a` and a neighborhood around the set `s` such that these two neighborhoods do not intersect. This property is a common one in regular spaces, a type of topological space, and is part of the definition of what it means for a space to be regular. More concisely: In a regular topological space, if a point is not in a closed set, then there exist disjoint open neighborhoods for the point and the set.
`T1Space.t1` theorem T1Space.t1 : ∀ {X : Type u} [inst : TopologicalSpace X] [self : T1Space X] (x : X), IsClosed {x} This theorem states that for any type 'X' that forms a topological space and additionally is a T₁ space, a set containing a single element 'x' from 'X' is a closed set. In terms of topology, a T₁ space is a topological space in which for every pair of distinct points, each has a neighborhood not containing the other. Therefore, in such a space, a singleton set (a set with only one element) is always a closed set. More concisely: In a T₁ topological space 'X', the singleton set {x} is closed for any point x in X.
`totallySeparatedSpace_of_t1_of_basis_clopen` theorem totallySeparatedSpace_of_t1_of_basis_clopen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X], TopologicalSpace.IsTopologicalBasis {s \| IsClopen s} → TotallySeparatedSpace X The theorem states that if we have a T1 space (a topological space where for any two distinct points, each has a neighborhood not containing the other) where the basis of the topology consists of sets that are both closed and open (clopen), then this space is totally separated. In other words, for every pair of distinct points in this space, there exists a clopen set that contains one of the points but not the other. More concisely: In a T1 space with a clopen basis, every pair of distinct points can be separated by a clopen set.
`exists_isOpen_singleton_of_isOpen_finite` theorem exists_isOpen_singleton_of_isOpen_finite : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T0Space X] {s : Set X}, s.Finite → s.Nonempty → IsOpen s → ∃ x ∈ s, IsOpen {x} The theorem `exists_isOpen_singleton_of_isOpen_finite` states that for any given finite open set `S` in a T0 space (a topological space where for any two distinct points there exists an open set containing one but not the other), there is some element `x` in `S` such that the set containing only `x` is open. In other words, in a T0 space, any finite open set will have at least one element that when isolated in a set by itself, the resulting set is considered open in the context of the topology. More concisely: In a T0 space, every finite open set contains an isolated point.
`t2_iff_ultrafilter` theorem t2_iff_ultrafilter : ∀ {X : Type u_1} [inst : TopologicalSpace X], T2Space X ↔ ∀ {x y : X} (f : Ultrafilter X), ↑f ≤ nhds x → ↑f ≤ nhds y → x = y This theorem states that a topological space 'X' is a T2 space (also known as a Hausdorff space) if and only if for any two points 'x' and 'y' in 'X' and any ultrafilter 'f' on 'X', if 'f' is included in the neighborhood filter of 'x' and the neighborhood filter of 'y', then 'x' must be equal to 'y'. In other words, no ultrafilter can be included in the neighborhood filters of two distinct points in a T2 space. The neighborhood filter of a point includes all the open sets that contain the point. An ultrafilter is a maximally consistent notion of largeness for subsets of a given set. The condition that 'f' is included in the neighborhood filter of a point means that the ultrafilter deems all the neighborhoods of the point as large. More concisely: A topological space is T2 (Hausdorff) if and only if no ultrafilter intersects the neighborhood filters of distinct points.
`compl_singleton_mem_nhds` theorem compl_singleton_mem_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] {x y : X}, y ≠ x → {x}ᶜ ∈ nhds y The theorem `compl_singleton_mem_nhds` states that for any topological space `X` that is also a T1 space and for any two distinct elements `x` and `y` in `X`, the complement of the singleton set containing `x` is a neighborhood of `y`. This means that there exists an open set around `y` that does not include `x`. More concisely: In a T1 topological space `X`, for distinct elements `x` and `y` in `X`, the complement of the singleton set `{x}` is a neighborhood of `y`.
`Filter.HasBasis.nhds_closure` theorem Filter.HasBasis.nhds_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : RegularSpace X] {ι : Sort u_3} {x : X} {p : ι → Prop} {s : ι → Set X}, (nhds x).HasBasis p s → (nhds x).HasBasis p fun i => closure (s i) This theorem states that for any topological space `X` that is also a regular space, and for any index type `ι`, any point `x` in `X`, and any predicate `p` on `ι` and set-valued function `s` from `ι` to the set of points in `X`, if the neighborhood filter at `x`, `nhds x`, has a basis characterized by the predicate `p` and the set-valued function `s`, then the neighborhood filter at `x` also has a basis characterized by the predicate `p` and the set-valued function that maps each index to the closure of the set `s i`. In simple terms, if a basis of open sets around a point in a regular topological space is given, then the basis remains valid when each open set is replaced by its closure. More concisely: In a regular topological space, if the neighborhood filter at a point has a basis characterized by a predicate and a set-valued function, then the basis remains valid with each set replaced by its closure.
`isOpen_compl_singleton` theorem isOpen_compl_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] {x : X}, IsOpen {x}ᶜ This theorem states that for any type `X`, which has a structure of a topological space, and an additional structure of a `T1Space` (which is a topological space where for every pair of distinct points there is an open set containing one but not the other), for any point `x` in `X`, the complement of the singleton set `{x}` is an open set. In mathematical terms, this means if we have a `T1` topological space, the complement of any singleton set is an open set in that space. More concisely: In a T1 topological space, the complement of any singleton set is an open set.
`nhds_inter_eq_singleton_of_mem_discrete` theorem nhds_inter_eq_singleton_of_mem_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [inst_1 : DiscreteTopology ↑s] {x : X}, x ∈ s → ∃ U ∈ nhds x, U ∩ s = {x} The theorem `nhds_inter_eq_singleton_of_mem_discrete` states that for any point `x` in a discrete subset `s` of a topological space, there exists a neighborhood of `x` that intersects with `s` only at `x`. In other words, given a topological space `X`, a discrete subset `s` of `X`, and a point `x` in `s`, we can always find a neighborhood `U` of `x` such that the intersection of `U` and `s` is precisely the singleton set `{x}`. This reflects a property of discrete sets in topological spaces: every point in a discrete set is "isolated" from other points in the set by neighborhoods that do not contain any other points from the set. More concisely: For any discrete subset `s` of a topological space `X` and any point `x` in `s`, there exists a neighborhood of `x` that intersects `s` only at `x`.
`R1Space.induced` theorem R1Space.induced : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : R1Space X] (f : Y → X), R1Space Y This theorem states that for any two types `X` and `Y`, where `X` is a topological space and also an `R1Space` (a space with separable points), and `f` is a function from `Y` to `X`, then `Y` is also an `R1Space`. In other words, the R1 space property (separability of points) is preserved under mapping from `Y` to `X`. More concisely: If `X` is an `R1Space` topological space and `f` is a function from an arbitrary topological space `Y` to `X`, then `Y` is an `R1Space`.
`SeparatedNhds.of_isCompact_isClosed` theorem SeparatedNhds.of_isCompact_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : RegularSpace X] {s t : Set X}, IsCompact s → IsClosed t → Disjoint s t → SeparatedNhds s t The theorem `SeparatedNhds.of_isCompact_isClosed` states that in a regular topological space, given a compact set and a closed set that are disjoint, there exist disjoint neighborhoods for these sets. In other words, it's possible to find two open sets such that the compact set is contained in one open set, the closed set is contained in the other open set, and these two open sets do not intersect. Regularity of a topological space is a property which guarantees the existence of such disjoint open sets. More concisely: In a regular topological space, given a compact and closed disjoint sets, there exist disjoint open neighborhoods for each set.
`IsCompact.binary_compact_cover` theorem IsCompact.binary_compact_cover : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {K U V : Set X}, IsCompact K → IsOpen U → IsOpen V → K ⊆ U ∪ V → ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂ The theorem `IsCompact.binary_compact_cover` states that for any type `X` with a topological structure and `R1Space` structure, given a compact set `K` and two open sets `U` and `V` in `X`, if `K` is a subset of the union of `U` and `V`, then there exist two compact subsets `K₁` and `K₂` of `X` such that `K₁` is a subset of `U`, `K₂` is a subset of `V`, and `K` is the union of `K₁` and `K₂`. This theorem thus asserts that a compact set covered by two open sets can be equivalently covered by two compact subsets. More concisely: Given a compact subset `K` of a topological space `X` with `R1Space` structure, there exist two compact subsets `K₁` and `K₂` such that `K = K₁ ∪ K₂` and `K₁ ⊆ U`, `K₂ ⊆ V`, for any open sets `U` and `V` containing `K`.
`T25Space.t2_5` theorem T25Space.t2_5 : ∀ {X : Type u} [inst : TopologicalSpace X] [self : T25Space X] ⦃x y : X⦄, x ≠ y → Disjoint ((nhds x).lift' closure) ((nhds y).lift' closure) This theorem states that in a T2.5 space (also known as a Urysohn space), for any two distinct points, the filters of their closed neighborhoods are disjoint. In other words, there is no closed neighborhood that contains both points. Here, a closed neighborhood of a point is the closure of an open set which contains the point, and a filter of closed neighborhoods for a point is a collection of these closed neighborhoods that follow certain rules, such as containing the whole space and being closed under intersection. The Disjoint function in this context means that the intersection of any closed neighborhood of the first point with any closed neighborhood of the second point is empty. More concisely: In a T2.5 space, the filters of the closed neighborhoods of any two distinct points are disjoint.
`Embedding.t0Space` theorem Embedding.t0Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T0Space Y] {f : X → Y}, Embedding f → T0Space X This theorem states that for any two types `X` and `Y`, given that `Y` is a T0 space and `f` is an embedding from `X` to `Y`, then `X` is also a T0 space. Here, a T0 space is a topological space that satisfies the T0 separation axiom, meaning that for any two distinct points in the space, there is at least one open set containing one of them but not the other. An embedding is a function `f` that is both injective (or one-to-one) and continuous, and its inverse function is also continuous when restricted to `f`'s range. More concisely: If `f` is an embedding of a T0 space `X` into a T0 space `Y`, then `X` is also a T0 space.
`lim_eq` theorem lim_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {f : Filter X} {x : X} [inst_2 : f.NeBot], f ≤ nhds x → lim f = x The theorem `lim_eq` is stating that for any topological space `X` which is also a `T2Space`, or in more common terms, a Hausdorff space, given a filter `f` on `X` that is not the bottom filter (`Filter.NeBot f`), if `f` is a subset of the neighbourhood filter of some element `x` in `X` (expressed as `f ≤ nhds x`), then the limit of the filter `f` must be the element `x` itself. In simpler terms, this theorem is saying that in a Hausdorff space, if a filter converges to some point, then the limit of the filter is indeed that point. More concisely: In a Hausdorff space, if a filter converges to an element, then the limit of the filter is that element.
`eq_of_tendsto_nhds` theorem eq_of_tendsto_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T1Space Y] {f : X → Y} {x : X} {y : Y}, Filter.Tendsto f (nhds x) (nhds y) → f x = y The theorem `eq_of_tendsto_nhds` states that if a function `f` from a topological space `X` to a `T1Space` `Y` has a limit of `y` at a point `x` (i.e., as the values of `f` get arbitrarily close to `y` when the input values get arbitrarily close to `x`), then `f(x)` must be equal to `y`. This is expressed in terms of filter theory, where `Filter.Tendsto f (nhds x) (nhds y)` encapsulates the concept of the limit of a function. The `T1Space` is a topological space where for each pair of distinct points, each point has an open neighborhood not containing the other point. More concisely: If a function `f` from a topological space `X` to a T1 space `Y` has the limit `y` at `x`, then `f(x) = y`.
`tendsto_nhds_unique` theorem tendsto_nhds_unique : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : T2Space X] {f : Y → X} {l : Filter Y} {a b : X} [inst_2 : l.NeBot], Filter.Tendsto f l (nhds a) → Filter.Tendsto f l (nhds b) → a = b The theorem `tendsto_nhds_unique` states that for any two types `X` and `Y`, where `X` is a topological space and also a T2 space (also known as a Hausdorff space), and given a function `f` from `Y` to `X` and a filter `l` on `Y` that is not a bottom filter, if `f` tends to the neighborhood filter of `a` along `l` and also tends to the neighborhood filter of `b` along `l`, then `a` must be equal to `b`. In other words, in a Hausdorff space, a function cannot converge to two different limits. More concisely: In a Hausdorff space, if a function converges to two different limits along the same filter, then those limits are equal.
`Set.InjOn.exists_mem_nhdsSet` theorem Set.InjOn.exists_mem_nhdsSet : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y] {f : X → Y} {s : Set X}, Set.InjOn f s → IsCompact s → (∀ x ∈ s, ContinuousAt f x) → (∀ x ∈ s, ∃ u ∈ nhds x, Set.InjOn f u) → ∃ t ∈ nhdsSet s, Set.InjOn f t The theorem `Set.InjOn.exists_mem_nhdsSet` states that if a function `f` from a topological space `X` to another topological space `Y` (which is a T2 space, or Hausdorff space) satisfies the following conditions: - `f` is injective on a compact set `s` of `X`, - `f` is continuous at every point of this set `s`, - for each point `x` in `s`, `f` is injective on some neighborhood of `x`, then there exists a neighborhood of the set `s` where `f` is injective. In other words, if `f` behaves nicely (is injective and continuous) in the compact set `s` and around each point in `s`, then this nice behavior (injectivity) can be extended to some larger neighborhood of the set `s`. More concisely: If a continuous, injective function between compact subsets of Hausdorff spaces satisfies injectivity on each point and in some neighborhood of each point, then it is injective on a neighborhood of the union of these points.
`separatedNhds_of_finset_finset` theorem separatedNhds_of_finset_finset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] (s t : Finset X), Disjoint s t → SeparatedNhds ↑s ↑t This theorem, `separatedNhds_of_finset_finset`, states that for any type `X` that has a topology and is a T2 space (also known as a Hausdorff space), given two finite sets `s` and `t` of elements of type `X` that are disjoint, the neighborhoods of the elements of the sets `s` and `t` (viewed as subsets of the topological space) are separated. In other words, there exist two open sets `U` and `V` such that `s` is contained in `U`, `t` is contained in `V`, and `U` and `V` are disjoint. This theorem is an alias of `SeparatedNhds.of_finset_finset`. More concisely: For any T2 topological space X and finite disjoint sets s and t in X, there exist open sets U and V such that s is contained in U and t is contained in V, with U and V being disjoint.
`loc_compact_t2_tot_disc_iff_tot_sep` theorem loc_compact_t2_tot_disc_iff_tot_sep : ∀ {H : Type u_3} [inst : TopologicalSpace H] [inst_1 : LocallyCompactSpace H] [inst_2 : T2Space H], TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H This theorem states that for any type `H` that has a topological space structure, a locally compact space structure, and a Hausdorff space (T2 space) structure, `H` is a totally disconnected space if and only if it is a totally separated space. In other words, in the context of locally compact Hausdorff spaces, total disconnectedness and total separateness are equivalent properties. More concisely: In the context of locally compact Hausdorff spaces, a space is totally disconnected if and only if it is totally separated.
`exists_mem_nhds_isCompact_isClosed` theorem exists_mem_nhds_isCompact_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] [inst_2 : WeaklyLocallyCompactSpace X] (x : X), ∃ K ∈ nhds x, IsCompact K ∧ IsClosed K The theorem `exists_mem_nhds_isCompact_isClosed` states that in a weakly locally compact `R₁` space, every point has a compact and closed neighborhood. More specifically, for any type `X` that has a topology and is also a `R₁` space and a weakly locally compact space, for every point `x` in `X`, there exists a set `K` which is a neighborhood of `x`, and additionally, `K` is both compact and closed. More concisely: In a weakly locally compact `R₁` space `X`, every point `x` has a compact and closed neighborhood.
`ClosedEmbedding.normalSpace` theorem ClosedEmbedding.normalSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y] {f : X → Y}, ClosedEmbedding f → NormalSpace X The theorem `ClosedEmbedding.normalSpace` states that for any two types `X` and `Y` with `X` and `Y` being topological spaces, and `Y` being a normal space, if there exists a closed embedding function from `X` to `Y`, then `X` is also a normal space. In terms of topology, this theorem confirms that normality is preserved under closed embeddings. More concisely: If a topological space `X` is closedly embedded into a normal space `Y`, then `X` is normal.
`disjoint_lift'_closure_nhds` theorem disjoint_lift'_closure_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T25Space X] {x y : X}, Disjoint ((nhds x).lift' closure) ((nhds y).lift' closure) ↔ x ≠ y The theorem states that for any topological space `X` that is also a T2.5 space, and for any two elements `x` and `y` of `X`, the closure of the neighborhood filters at `x` and `y` are disjoint if and only if `x` and `y` are not equal. In other words, if we have two distinct points in a T2.5 space, then the smallest closed sets containing the open sets around these points do not overlap. In this context, 'disjoint' means that the infimum (greatest lower bound) of the two sets is the bottom element of the lattice of sets, which corresponds to the empty set in this case. More concisely: In a T2.5 topological space, the closure of the neighborhood filters at distinct points are disjoint.
`Inseparable.eq` theorem Inseparable.eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T0Space X] {x y : X}, Inseparable x y → x = y The theorem `Inseparable.eq` asserts that for any topological space `X` with a `T0` separation axiom, if two points `x` and `y` in `X` are `Inseparable` — that is, if the neighborhoods of `x` and `y` are the same — then `x` is equal to `y`. This theorem provides a condition under which two points in a `T0` topological space can be proven to be identical, based on the properties of their respective neighborhoods. More concisely: In a T0 topological space, if two points have identical neighborhood systems, then they are equal.
`Set.Finite.t2_separation` theorem Set.Finite.t2_separation : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {s : Set X}, s.Finite → ∃ U, (∀ (x : X), x ∈ U x ∧ IsOpen (U x)) ∧ s.PairwiseDisjoint U The theorem `Set.Finite.t2_separation` states the following: For any type `X` equipped with a topological space structure and a `T2` (Hausdorff) space structure, and for any finite set `s` of type `Set X`, there exists a collection of open sets `U`, such that every element `x` of `X` is both a member of its corresponding open set in `U` and the open set `U x` is an open set in the topological space. Furthermore, these open sets `U x` are pairwise disjoint for each element in the set `s`. In other words, in a Hausdorff space, we can find open sets to separate each pair of distinct points in a finite set. More concisely: In a T2 topological space, for any finite subset, there exist pairwise disjoint open sets, each containing a point from the subset and containing that point's closure in its interior.
`TopologicalSpace.subset_trans` theorem TopologicalSpace.subset_trans : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} (ts : t ⊆ s), instTopologicalSpaceSubtype = TopologicalSpace.induced (Set.inclusion ts) instTopologicalSpaceSubtype This theorem states that for a topological space `X` and two subsets `s` and `t` of `X`, if `t` is a subset of `s`, then the topological space structure on `t` induced by `X` is equivalent to the one that is obtained via the induced topological space structure on `s`. The equivalence is established through the inclusion function from `t` to `s`. In other words, the topology on a subset `t` of `s` induced directly from the parent space `X` is the same as the one obtained by first inducing a topology on `s` from `X` and then restricting it to `t` through the inclusion map. More concisely: The topology on a subset `t` of a topological space `X` induced directly from `X` is equivalent to the restricted topology obtained from the topology induced on `s` (containing `t`) from `X`.
`continuousAt_of_tendsto_nhds` theorem continuousAt_of_tendsto_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T1Space Y] {f : X → Y} {x : X} {y : Y}, Filter.Tendsto f (nhds x) (nhds y) → ContinuousAt f x The theorem `continuousAt_of_tendsto_nhds` states that for any function `f` from a topological space `X` to a `T1Space` `Y`, if `f` has a limit at a point `x` in `X` that tends to some `y` in `Y` (i.e., for any neighborhood of `y`, the preimage of it under `f` is a neighborhood of `x`), then `f` is continuous at `x`. The condition of `Y` being a `T1Space` adds the requirement that for every distinct pair of points in `Y`, each has a neighborhood not containing the other. More concisely: If a function `f` from a topological space `X` to a `T1Space` `Y` has a limit at `x` in `X` that tends to `y` in `Y`, then `f` is continuous at `x`.
`insert_mem_nhdsWithin_of_subset_insert` theorem insert_mem_nhdsWithin_of_subset_insert : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] {x y : X} {s t : Set X}, t ⊆ insert y s → insert x s ∈ nhdsWithin x t This theorem states that for any topological space `X` that also has `T1` separation axiom, given any two points `x` and `y` in `X` and any two sets `s` and `t` of type `X`, if `t` is a subset of the set obtained by adding `y` to `s`, then the set obtained by adding `x` to `s` is a neighborhood of `x` within `t`. Here, a neighborhood of `x` within `t` means a set that contains the intersection of `t` and a neighborhood of `x`. The `T1` separation axiom is a property of topological spaces where for any two distinct points, each has a neighborhood not containing the other. More concisely: Given any topological space `X` with the `T1` separation axiom, if `s ⊆ t ∋ y` and `N` is a neighborhood of `x` in `X`, then `(s ∪ {y}) ∩ N` is a neighborhood of `x` within `t`.
`Continuous.closedEmbedding` theorem Continuous.closedEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : CompactSpace X] [inst_3 : T2Space Y] {f : X → Y}, Continuous f → Function.Injective f → ClosedEmbedding f The theorem `Continuous.closedEmbedding` states that for any two types `X` and `Y` endowed with topological structures, and assuming that `X` is a compact space and `Y` is a Hausdorff space (or `T2` space), any continuous and injective function `f` mapping `X` to `Y` is a closed embedding. In the context of topological spaces, a closed embedding is a function which is both an embedding and also its image is closed in the codomain. This theorem is a significant result in topology linking compactness, Hausdorff property, continuity, and injectiveness to the property of being a closed embedding. More concisely: Given compact and Hausdorff topological spaces X and Y, a continuous, injective function from X to Y is a closed embedding.
`Embedding.t1Space` theorem Embedding.t1Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T1Space Y] {f : X → Y}, Embedding f → T1Space X This theorem states that for any two types `X` and `Y`, if `Y` is a T1 space (meaning that for any two distinct points in `Y`, they each have a neighborhood that does not contain the other point), and if there exists a function `f` from `X` to `Y` that is an embedding (a function that preserves the topological structure), then `X` is also a T1 space. The topological structures of `X` and `Y` are given by the instances `inst` and `inst_1` respectively. More concisely: If `X` is a topological space, `Y` is a T1 space, and `f : X → Y` is an embedding, then `X` is a T1 space.
`Mathlib.Topology.Separation._auxLemma.2` theorem Mathlib.Topology.Separation._auxLemma.2 : ∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, (b ∧ ∃ x, p x) = ∃ x, b ∧ p x This theorem, named `Mathlib.Topology.Separation._auxLemma.2`, states that for any type `α`, any predicate `p` on `α`, and any proposition `b`, the conjunction of `b` and the existence of an element of `α` satisfying `p` is logically equivalent to the existence of an element of `α` such that `b` and `p` both hold for that element. In other words, it's stating that the proposition `b` can be distributed inside the existential quantifier. More concisely: For any type `α`, proposition `b`, and predicate `p` on `α`, the statements `∃x : α, p x ∧ b` and `∃x : α, p x ∧ b holds` are logically equivalent.
`regularSpace_TFAE` theorem regularSpace_TFAE : ∀ (X : Type u) [inst : TopologicalSpace X], [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (nhdsSet s) (nhds x), ∀ (x : X) (s : Set X), Disjoint (nhdsSet s) (nhds x) ↔ x ∉ closure s, ∀ (x : X), ∀ s ∈ nhds x, ∃ t ∈ nhds x, IsClosed t ∧ t ⊆ s, ∀ (x : X), (nhds x).lift' closure ≤ nhds x, ∀ (x : X), (nhds x).lift' closure = nhds x].TFAE This theorem states that for any type `X` and an associated topological space, the following propositions are equivalent: 1. `X` is a regular space. In topology, a regular space is a topological space that, intuitively, has enough room to distinguish points from closed sets, i.e., for any point and any closed set not containing that point, there are disjoint open sets containing the point and the closed set, respectively. 2. For any set `s` in `X` and any point `x` not in the closure of `s`, the filter of neighborhoods of `s` and the filter of neighborhoods of `x` are disjoint. The closure of a set is the smallest closed set containing the original set, and the filter of neighborhoods of a set is essentially the union of the neighborhoods of its points. 3. For any point `x` in `X` and any set `s` in `X`, the filter of neighborhoods of `s` and the filter of neighborhoods of `x` are disjoint if and only if `x` is not in the closure of `s`. 4. For any point `x` in `X` and any set `s` in the neighborhoods of `x`, there exists a closed set `t` in the neighborhoods of `x` such that `t` is a subset of `s`. 5. For any point `x` in `X`, the filter obtained by lifting the closure operation to the neighborhoods of `x` is less than or equal to the filter of neighborhoods of `x`. 6. For any point `x` in `X`, the filter obtained by lifting the closure operation to the neighborhoods of `x` is equal to the filter of neighborhoods of `x`. These propositions are fundamental in the study of the topology of a space, and their equivalence implies that they could be used interchangeably in the topological analysis of a given space. More concisely: A topological space `X` is regular if and only if for any point `x` in `X` and any set `s` not containing `x`, the filters of neighborhoods of `s` and `x` are disjoint.
`isCompact_isClosed_basis_nhds` theorem isCompact_isClosed_basis_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] [inst_2 : WeaklyLocallyCompactSpace X] (x : X), (nhds x).HasBasis (fun K => K ∈ nhds x ∧ IsCompact K ∧ IsClosed K) fun x => x This theorem states that in a weakly locally compact R₁ space, the set of compact closed neighborhoods of a point `x` forms a basis for the neighborhood filter at `x`. In other words, any neighborhood of `x` can be expressed as a union of these compact closed neighborhoods. Here, a space is weakly locally compact if every point has a compact neighborhood, and a space is R₁ if any two distinct points have disjoint neighborhood filters. The compact closed neighborhoods are subsets of the space that are both compact (for any nontrivial filter that contains the subset, there exists a point in the subset where every set of the filter intersects every neighborhood of the point) and closed (their complement is an open set). More concisely: In a weakly locally compact and R₁ space, the set of compact closed neighborhoods of a point forms a basis for its neighborhood filter.
`Ne.nhdsWithin_compl_singleton` theorem Ne.nhdsWithin_compl_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] {x y : X}, x ≠ y → nhdsWithin x {y}ᶜ = nhds x This theorem states that for any type `X` with a topological space structure and a `T1Space` structure (i.e., any singleton set is closed), and for any two distinct points `x` and `y` from `X`, the neighborhood within the complement of the singleton set `{y}` at the point `x` is the same as the neighborhood of `x`. In other words, if `x` and `y` are different points in a topological space where singletons are closed, then the filter of sets that intersect the complement of `{y}` and contain an open set around `x`, is the same as the filter of all open sets containing `x`. More concisely: In a T1 topological space, for distinct points `x` and `y`, the neighborhood filters of `x` in the complement of `{y}` and at `x` are equal.
`T5Space.completely_normal` theorem T5Space.completely_normal : ∀ {X : Type u} [inst : TopologicalSpace X] [self : T5Space X] ⦃s t : Set X⦄, Disjoint (closure s) t → Disjoint s (closure t) → Disjoint (nhdsSet s) (nhdsSet t) The theorem `T5Space.completely_normal` states that for any topological space `X` that satisfies the T5 separation axiom (also known as being completely normal), given two sets `s` and `t` such that the closure of `s` is disjoint with `t` and `s` is disjoint with the closure of `t`, then there exist disjoint neighborhoods of `s` and `t`. In simple terms, if two sets do not overlap in `X` nor do their closure, they have separate surrounding neighborhoods. More concisely: In a T5 space, disjoint sets with closed disjoint closures have disjoint open neighborhoods.
`disjoint_nhdsWithin_of_mem_discrete` theorem disjoint_nhdsWithin_of_mem_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [inst_1 : DiscreteTopology ↑s] {x : X}, x ∈ s → ∃ U ∈ nhdsWithin x {x}ᶜ, Disjoint U s The theorem `disjoint_nhdsWithin_of_mem_discrete` states that for any point `x` in a discrete subset `s` of a topological space `X`, there exists a set `U` with two properties. First, `U` is a punctured neighborhood of `x` - meaning the union of `U` and the singleton set containing `x` forms a neighborhood of `x`. Second, the set `U` is disjoint from the set `s`. This indicates that there is no common element between set `U` and set `s`. The concept of a discrete subset refers to a topology where every subset is an open set. More concisely: For any discrete subset `s` of a topological space `X` and any point `x` in `s`, there exists a punctured neighborhood `U` of `x` that is disjoint from `s`.
`Set.InjOn.exists_isOpen_superset` theorem Set.InjOn.exists_isOpen_superset : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y] {f : X → Y} {s : Set X}, Set.InjOn f s → IsCompact s → (∀ x ∈ s, ContinuousAt f x) → (∀ x ∈ s, ∃ u ∈ nhds x, Set.InjOn f u) → ∃ t, IsOpen t ∧ s ⊆ t ∧ Set.InjOn f t This theorem states that if a function `f` satisfies the following conditions: - It is injective (i.e., it maps distinct inputs to distinct outputs) on a compact set `s`; - It is continuous (i.e., small changes in the input result in arbitrarily small changes in the output) at every point of this set; - For every point in this set, there is a neighborhood of the point where the function is injective; Then there exists an open neighborhood of this set where the function is injective. In other words, we can find an open set that contains our original set `s` and preserves the injective property of our function. More concisely: If a function `f` is injective, continuous, and for every point in a compact set `s`, there exists an open neighborhood where `f` is injective, then `f` is injective on some open neighborhood of `s`.
`exists_compact_superset_iff` theorem exists_compact_superset_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {s : Set X}, (∃ K, IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure s) This theorem, `exists_compact_superset_iff`, states that for any topological space `X` equipped with the `R1Space` property and any set `s` in `X`, the existence of a compact superset `K` of `s` is equivalent to the closure of `s` being compact. In other words, there exists a compact set `K` such that `s` is a subset of `K` if and only if the closure of `s` is a compact set. Here, a set is called compact if for every nontrivial filter that contains the set, there exists an element in the set such that every set in the filter intersects every neighborhood of that element. The closure of a set is the smallest closed set that contains the set. More concisely: A set in a topological space with the R1Space property has a compact superset if and only if its closure is a compact set.
`SeparatedNhds.of_isCompact_isCompact_isClosed` theorem SeparatedNhds.of_isCompact_isCompact_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {K L : Set X}, IsCompact K → IsCompact L → IsClosed L → Disjoint K L → SeparatedNhds K L This theorem states that in an R₁ topological space, if there are two disjoint compact sets `K` and `L` and `L` is also a closed set, then there exist disjoint neighborhoods of `K` and `L`. This means that there are open sets `U` and `V` such that `K` is contained in `U`, `L` is contained in `V`, and `U` and `V` are disjoint, i.e., their intersection is empty. More concisely: In an R₁ topological space, if two disjoint compact-and-closed sets `K` and `L` exist, then there exist disjoint open sets `U` and `V` such that `K` is contained in `U` and `L` is contained in `V`.
`IsCompact.inter` theorem IsCompact.inter : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {s t : Set X}, IsCompact s → IsCompact t → IsCompact (s ∩ t) The theorem `IsCompact.inter` states that for any type `X` with a topology and a `T2Space` (Hausdorff space) structure, if `s` and `t` are two sets in `X` that are both compact, then their intersection `s ∩ t` is also compact. In other words, in a Hausdorff space, the intersection of two compact sets is also a compact set. More concisely: In a Hausdorff space, the intersection of two compact sets is a compact set.
`IsCompact.isClosed` theorem IsCompact.isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {s : Set X}, IsCompact s → IsClosed s The theorem states that in a T2 Space (also known as a Hausdorff space), any set that is compact is also closed. In other words, given a topological space that satisfies the T2 separation axiom, if a set within that space has the property of compactness (meaning, for any nontrivial filter that contains the set, there exists a point in the set such that every set of the filter intersects every neighborhood of the point), then this set also has the property of being closed (its complement is an open set). More concisely: In a T2 (Hausdorff) space, every compact set is closed.
`closure_singleton` theorem closure_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] {x : X}, closure {x} = {x} The theorem `closure_singleton` states that for any type `X` equipped with a topology (represented by `TopologicalSpace X`) and having the T1 separation axiom (`T1Space X`), for any element `x` of `X`, the closure of the singleton set `{x}` is equal to the set `{x}` itself. In other words, in a T1 space, the closure of a set containing a single point is just the set containing that point. More concisely: In a T1 topological space, the closure of a singleton set is equal to that set.
`isClosed_eq` theorem isClosed_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space X] {f g : Y → X}, Continuous f → Continuous g → IsClosed {y \| f y = g y} This theorem states that for any types `X` and `Y` where `X` is a Hausdorff (or T2) space and there are topological spaces defined on `X` and `Y`, if `f` and `g` are continuous functions from `Y` to `X`, then the set of all `y` in `Y` such that `f(y) = g(y)` is a closed set in the topological space `Y`. In other words, the set of points where the two continuous functions coincide is a closed set. More concisely: If `X` is a Hausdorff space and `f` and `g` are continuous functions from a topological space `Y` to `X`, then the graph of their equality, `{y : Y \| f(y) = g(y)}`, is a closed subset of `Y`.
`T2Space.t2` theorem T2Space.t2 : ∀ {X : Type u} [inst : TopologicalSpace X] [self : T2Space X], Pairwise fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v This theorem states that for every pair of distinct points in a Hausdorff space (a topological space that satisfies the T2 separation axiom), there exist two open neighborhoods (one for each point) that do not have any common points. In other words, these open neighborhoods are disjoint. The Hausdorff property ensures the separation of points, helping to avoid many pathological cases in analysis and topology. More concisely: In a Hausdorff space, for every pair of distinct points, there exist disjoint open neighborhoods.
`Filter.coclosedCompact_eq_cocompact` theorem Filter.coclosedCompact_eq_cocompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X], Filter.coclosedCompact X = Filter.cocompact X This theorem states that in any R₁ space, which is a type of topological space, the filters `coclosedCompact` and `cocompact` are equivalent. The `coclosedCompact` filter is generated by the complements of closed compact sets, while the `cocompact` filter is generated by the complements of compact sets. In simpler terms, it says that in an R₁ space, taking the complements of all compact sets or the complements of all closed compact sets generate the same filters. More concisely: In an R₁ space, the filters generated by the complements of compact sets and the complements of closed compact sets are equivalent.
`disjoint_nested_nhds` theorem disjoint_nested_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T3Space X] {x y : X}, x ≠ y → ∃ U₁ ∈ nhds x, ∃ V₁ ∈ nhds x, ∃ U₂ ∈ nhds y, ∃ V₂ ∈ nhds y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂ Given a topological space `X` that also satisfies the T3 separation axiom, and two distinct points `x` and `y` in `X`, the theorem asserts the existence of specific types of neighborhoods for `x` and `y`. Specifically, there exist neighborhoods `U₁` and `V₁` for `x`, and `U₂` and `V₂` for `y`, such that `U₁` and `U₂` are open, `V₁` and `V₂` are closed, `V₁` is a subset of `U₁`, `V₂` is a subset of `U₂`, and `U₁` and `U₂` are disjoint, i.e., their intersection is empty. This theorem thus guarantees the ability to separate `x` and `y` with these specially characterized neighborhoods. More concisely: In a T3 topological space, given distinct points `x` and `y`, there exist open sets `U₁` and `U₂`, and closed sets `V₁` and `V₂`, such that `x ∈ U₁ ∩ V₁`, `y ∈ U₂ ∩ V₂`, `U₁ ∩ U₂ = ∅`, and `V₁ ⊆ U₁` and `V₂ ⊆ U₂`.

LeanAide GPT-4 documentation

Module: Mathlib.Topology.Separation

separatedNhds_of_isCompact_isClosed

theorem separatedNhds_of_isCompact_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : RegularSpace X] {s t : Set X}, IsCompact s → IsClosed t → Disjoint s t → SeparatedNhds s t

IsClosed.exists_closed_singleton

theorem IsClosed.exists_closed_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T0Space X] [inst_2 : CompactSpace X] {S : Set X}, IsClosed S → S.Nonempty → ∃ x ∈ S, IsClosed {x}

separatedNhds_of_isCompact_isCompact_isClosed

theorem separatedNhds_of_isCompact_isCompact_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {K L : Set X}, IsCompact K → IsCompact L → IsClosed L → Disjoint K L → SeparatedNhds K L

exists_open_between_and_isCompact_closure

theorem exists_open_between_and_isCompact_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LocallyCompactSpace X] [inst_2 : RegularSpace X] {K U : Set X}, IsCompact K → IsOpen U → K ⊆ U → ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)

isOpen_inter_eq_singleton_of_mem_discrete

theorem isOpen_inter_eq_singleton_of_mem_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [inst_1 : DiscreteTopology ↑s] {x : X}, x ∈ s → ∃ U, IsOpen U ∧ U ∩ s = {x}

ClosedEmbedding.t4Space

theorem ClosedEmbedding.t4Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T4Space Y] {f : X → Y}, ClosedEmbedding f → T4Space X

Mathlib.Topology.Separation._auxLemma.47

theorem Mathlib.Topology.Separation._auxLemma.47 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : T1Space X] {l : Filter Y} [inst_2 : l.NeBot] {c d : X}, Filter.Tendsto (fun x => c) l (nhds d) = (c = d)

not_preirreducible_nontrivial_t2

theorem not_preirreducible_nontrivial_t2 : ∀ (X : Type u_4) [inst : TopologicalSpace X] [inst_1 : PreirreducibleSpace X] [inst_2 : Nontrivial X] [inst : T2Space X], False

isOpen_ne

theorem isOpen_ne : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] {x : X}, IsOpen {y | y ≠ x} := by sorry

specializes_iff_inseparable

theorem specializes_iff_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R0Space X] {x y : X}, x ⤳ y ↔ Inseparable x y

loc_compact_Haus_tot_disc_of_zero_dim

theorem loc_compact_Haus_tot_disc_of_zero_dim : ∀ {H : Type u_3} [inst : TopologicalSpace H] [inst_1 : LocallyCompactSpace H] [inst_2 : T2Space H] [inst_3 : TotallyDisconnectedSpace H], TopologicalSpace.IsTopologicalBasis {s | IsClopen s}

exists_mem_nhds_isClosed_subset

theorem exists_mem_nhds_isClosed_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : RegularSpace X] {x : X} {s : Set X}, s ∈ nhds x → ∃ t ∈ nhds x, IsClosed t ∧ t ⊆ s

Set.Finite.isClosed

theorem Set.Finite.isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] {s : Set X}, s.Finite → IsClosed s

t0Space_iff_inseparable

theorem t0Space_iff_inseparable : ∀ (X : Type u) [inst : TopologicalSpace X], T0Space X ↔ ∀ (x y : X), Inseparable x y → x = y

Inducing.injective

theorem Inducing.injective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T0Space X] {f : X → Y}, Inducing f → Function.Injective f

specializes_comm

theorem specializes_comm : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R0Space X] {x y : X}, x ⤳ y ↔ y ⤳ x

exists_open_with_compact_closure

theorem exists_open_with_compact_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] [inst_2 : WeaklyLocallyCompactSpace X] (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)

t1Space_TFAE

point_disjoint_finset_opens_of_t2

theorem point_disjoint_finset_opens_of_t2 : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {x : X} {s : Finset X}, x ∉ s → SeparatedNhds {x} ↑s

SeparatedNhds.disjoint_nhdsSet

theorem SeparatedNhds.disjoint_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → Disjoint (nhdsSet s) (nhdsSet t)

t1Space_iff_specializes_imp_eq

theorem t1Space_iff_specializes_imp_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X], T1Space X ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y

Embedding.t3Space

theorem Embedding.t3Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T3Space Y] {f : X → Y}, Embedding f → T3Space X

connectedComponent_eq_iInter_isClopen

theorem connectedComponent_eq_iInter_isClopen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : CompactSpace X] (x : X), connectedComponent x = ⋂ s, ↑s

SeparatedNhds.of_isCompact_isCompact

theorem SeparatedNhds.of_isCompact_isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {s t : Set X}, IsCompact s → IsCompact t → Disjoint s t → SeparatedNhds s t

IsCompact.closure_subset_of_isOpen

theorem IsCompact.closure_subset_of_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {K : Set X}, IsCompact K → ∀ {U : Set X}, IsOpen U → K ⊆ U → closure K ⊆ U

closed_nhds_basis

theorem closed_nhds_basis : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : RegularSpace X] (x : X), (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsClosed s) id

eq_of_nhds_neBot

theorem eq_of_nhds_neBot : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] {x y : X}, (nhds x ⊓ nhds y).NeBot → x = y := by sorry

IsCompact.isCompact_isClosed_basis_nhds

theorem IsCompact.isCompact_isClosed_basis_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {x : X} {L : Set X}, IsCompact L → L ∈ nhds x → (nhds x).HasBasis (fun K => K ∈ nhds x ∧ IsCompact K ∧ IsClosed K) fun x => x

nhdsWithin_of_mem_discrete

theorem nhdsWithin_of_mem_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [inst_1 : DiscreteTopology ↑s] {x : X}, x ∈ s → nhdsWithin x s = pure x

Embedding.t2Space

theorem Embedding.t2Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y] {f : X → Y}, Embedding f → T2Space X

RegularSpace.ofBasis

theorem RegularSpace.ofBasis : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : X → Sort u_3} {p : (a : X) → ι a → Prop} {s : (a : X) → ι a → Set X}, (∀ (a : X), (nhds a).HasBasis (p a) (s a)) → (∀ (a : X) (i : ι a), p a i → IsClosed (s a i)) → RegularSpace X

SeparatedNhds.symm

theorem SeparatedNhds.symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → SeparatedNhds t s

infinite_of_mem_nhds

theorem infinite_of_mem_nhds : ∀ {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : T1Space X] (x : X) [hx : (nhdsWithin x {x}ᶜ).NeBot] {s : Set X}, s ∈ nhds x → s.Infinite

isOpen_singleton_of_finite_mem_nhds

theorem isOpen_singleton_of_finite_mem_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T1Space X] (x : X) {s : Set X}, s ∈ nhds x → s.Finite → IsOpen {x}

Mathlib.Topology.Separation._auxLemma.4

theorem Mathlib.Topology.Separation._auxLemma.4 : ∀ {a b : Prop}, (a ∧ b) = (b ∧ a)

Specializes.inseparable

theorem Specializes.inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R0Space X] {x y : X}, x ⤳ y → Inseparable x y

IsCompact.closure_of_subset

theorem IsCompact.closure_of_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {s K : Set X}, IsCompact K → s ⊆ K → IsCompact (closure s)

Set.EqOn.closure

theorem Set.EqOn.closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space X] {s : Set Y} {f g : Y → X}, Set.EqOn f g s → Continuous f → Continuous g → Set.EqOn f g (closure s)

exists_subset_nhds_of_isCompact

IsCompact.mem_closure_iff_exists_inseparable

theorem IsCompact.mem_closure_iff_exists_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X] {y : X} {K : Set X}, IsCompact K → (y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y)

`separatedNhds_of_isCompact_isClosed`

`IsClosed.exists_closed_singleton`

`separatedNhds_of_isCompact_isCompact_isClosed`

`exists_open_between_and_isCompact_closure`

`isOpen_inter_eq_singleton_of_mem_discrete`

`ClosedEmbedding.t4Space`

`Mathlib.Topology.Separation._auxLemma.47`

`not_preirreducible_nontrivial_t2`

`isOpen_ne`

`specializes_iff_inseparable`

`loc_compact_Haus_tot_disc_of_zero_dim`

`exists_mem_nhds_isClosed_subset`

`Set.Finite.isClosed`

`t0Space_iff_inseparable`

`Inducing.injective`

`specializes_comm`

`exists_open_with_compact_closure`

`t1Space_TFAE`

`point_disjoint_finset_opens_of_t2`

`SeparatedNhds.disjoint_nhdsSet`

`t1Space_iff_specializes_imp_eq`

`Embedding.t3Space`

`connectedComponent_eq_iInter_isClopen`

`SeparatedNhds.of_isCompact_isCompact`

`IsCompact.closure_subset_of_isOpen`

`closed_nhds_basis`

`eq_of_nhds_neBot`

`IsCompact.isCompact_isClosed_basis_nhds`

`nhdsWithin_of_mem_discrete`

`Embedding.t2Space`

`RegularSpace.ofBasis`

`SeparatedNhds.symm`

`infinite_of_mem_nhds`

`isOpen_singleton_of_finite_mem_nhds`

`Mathlib.Topology.Separation._auxLemma.4`

`Specializes.inseparable`

`IsCompact.closure_of_subset`

`Set.EqOn.closure`

`exists_subset_nhds_of_isCompact`

`IsCompact.mem_closure_iff_exists_inseparable`

`specializes_iff_eq`

`exists_open_superset_and_isCompact_closure`

`Mathlib.Topology.Separation._auxLemma.65`

`Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete`

`compact_t2_tot_disc_iff_tot_sep`

`Specializes.eq`

`t2_iff_nhds`

`exists_isOpen_superset_and_isCompact_closure`

`compact_exists_isClopen_in_isOpen`

`exists_isOpen_mem_isCompact_closure`

`separated_by_continuous`

`Set.EqOn.of_subset_closure`

`Mathlib.Topology.Separation._auxLemma.8`

`isCompact_closure_of_subset_compact`

`Specializes.symm`

`t2_iff_isClosed_diagonal`

`Continuous.isClosedMap`

`Inducing.embedding`

`T2Space.of_injective_continuous`

`Mathlib.Topology.Separation._auxLemma.5`

`NormalSpace.normal`

`Continuous.ext_on`

`isClosed_singleton`

`disjoint_nhds_nhds`

`Mathlib.Topology.Separation._auxLemma.3`

`T0Space.t0`

`t2Space_iff_disjoint_nhds`

`Dense.diff_finite`

`IsCompact.closure_eq_biUnion_closure_singleton`

`QuotientMap.of_surjective_continuous`

`Filter.Tendsto.limUnder_eq`

`Dense.diff_singleton`

`Dense.diff_finset`

`IsCompact.closure`