IsGenericPoint.eq
theorem IsGenericPoint.eq :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x y : α} {S : Set α} [inst_1 : T0Space α],
IsGenericPoint x S → IsGenericPoint y S → x = y
This theorem states that in a T₀ space (a topological space satisfying the T₀ separation axiom), each set can have at most one generic point. Here, a point is considered generic for a set if the closure of the singleton set containing just that point equals the original set. Specifically, if `x` and `y` are both claimed to be generic points of the same set `S` in such a space, then `x` must equal `y`. Thus, it ensures uniqueness of the generic point for any given set in a T₀ space.
More concisely: In a T₀ space, each set has at most one generic point.
|
genericPoint_spec
theorem genericPoint_spec :
∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : QuasiSober α] [inst_2 : IrreducibleSpace α],
IsGenericPoint (genericPoint α) ⊤
The theorem `genericPoint_spec` states that for any type `α`, which is endowed with a topological structure, is quasi-sober, and is an irreducible space, the generic point of `α` is a generic point of the entire space (denoted by `⊤`). In other words, the closure of the set containing only the generic point of `α` is the entire space itself.
More concisely: The generic point of a quasi-sober, irreducible topological space is its own closure.
|
IsGenericPoint.mem
theorem IsGenericPoint.mem :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {S : Set α}, IsGenericPoint x S → x ∈ S
This theorem states that for any type `α` equipped with a topological space structure, any point `x` of type `α`, and any set `S` of elements of type `α`, if `x` is a generic point of `S`, then `x` is an element of `S`. Here, a point `x` being generic means that the closure of the singleton set containing `x` equals `S`. In mathematical notation, this is saying that if `S` is the closure of `{x}`, then `x` belongs to `S`.
More concisely: If a point is the generic element of a set in a topological space, then it belongs to that set.
|
IsGenericPoint.specializes
theorem IsGenericPoint.specializes :
∀ {α : Type u_1} [inst : TopologicalSpace α] {x y : α} {S : Set α}, IsGenericPoint x S → y ∈ S → x ⤳ y
This theorem states that for any topological space `α` and any two points `x` and `y` in `α`, along with a set `S` of points in `α`, if `x` is a generic point of `S` and `y` is an element of `S`, then `x` specializes to `y`. In the context of topology, "specializes to" means that every neighborhood of `x` also contains `y`, symbolized by `x ⤳ y`. This theorem essentially establishes a connection between the concept of a generic point and the specialization order in topological spaces.
More concisely: Given any topological space `α`, if point `x` is a generic point of set `S` and `y` is an element of `S`, then `x` specializes to `y` (i.e., every neighborhood of `x` contains `y`).
|
quasiSober_of_open_cover
theorem quasiSober_of_open_cover :
∀ {α : Type u_1} [inst : TopologicalSpace α] (S : Set (Set α)),
(∀ (s : ↑S), IsOpen ↑s) → ∀ [hS' : ∀ (s : ↑S), QuasiSober ↑↑s], S.sUnion = ⊤ → QuasiSober α
The theorem `quasiSober_of_open_cover` states that for any type `α` equipped with a topological space structure, if there exists a set `S` of subsets of `α` such that each element `s` of `S` is an open set and each `s` is also quasi sober, and the union of all elements in `S` equals the whole space `α`, then `α` itself is quasi sober. In other words, a space is quasi sober if it can be covered by open quasi sober subsets.
More concisely: If a topological space `α` can be covered by a collection of open and quasi sober subsets, then `α` is quasi sober.
|
IsIrreducible.genericPoint_spec
theorem IsIrreducible.genericPoint_spec :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : QuasiSober α] {S : Set α} (hS : IsIrreducible S),
IsGenericPoint hS.genericPoint (closure S)
The theorem `IsIrreducible.genericPoint_spec` states that for any type `α` with a topology and a quasi-sober property, and for any set `S` of type `α` that is irreducible, the generic point of the irreducible set `S` is a generic point of the closure of `S`. This means that the closure of the set containing only the generic point of `S` equals the closure of `S` itself. In mathematical terms, if `S` is an irreducible subset of a quasi-sober topological space, then the closure of `{x}`, where `x` is a generic point of `S`, is equal to the closure of `S`.
More concisely: For any irreducible subset S of a quasi-sober topological space, the generic point of S is a generic point of its closure. In other words, the closure of the singleton set containing the generic point of S equals the closure of S.
|