TopologicalSpace.Opens.eq_bot_or_top
theorem TopologicalSpace.Opens.eq_bot_or_top :
∀ {α : Type u_5} [t : TopologicalSpace α], t = ⊤ → ∀ (U : TopologicalSpace.Opens α), U = ⊥ ∨ U = ⊤
The theorem `TopologicalSpace.Opens.eq_bot_or_top` states that for any type `α` and a topological space `t` of this type, if `t` is equal to the indiscrete (or trivial) topology (denoted as `⊤`), then any open set `U` of this topological space is either empty (denoted as `⊥`) or equal to the whole space (`⊤`). In essence, it says that in the indiscrete topology, the only open sets are the empty set and the whole space itself.
More concisely: In the indiscrete topology on a type `α`, every open set is either the empty set or the whole space.
|
TopologicalSpace.Opens.iSup_def
theorem TopologicalSpace.Opens.iSup_def :
∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Sort u_5} (s : ι → TopologicalSpace.Opens α),
⨆ i, s i = { carrier := ⋃ i, ↑(s i), is_open' := ⋯ }
This theorem states that for any type `α` equipped with a topological space structure, and for any indexed collection of open sets `s`, indexed over an arbitrary `ι`, the supremum (i.e., the least upper bound) of this collection, denoted by `⨆ i, s i`, is defined to be the open set whose carrier (i.e., underlying set) is the union of the carriers of the elements of `s`, and whose 'is_open' status is suppressed in the theorem statement.
In the context of topology, this theorem essentially says that the supremum of a collection of open sets is the open set formed by taking the union of all the sets in the collection.
More concisely: The supremum of an indexed collection of open sets in a topological space is the open set with the union of their underlying sets.
|
TopologicalSpace.Opens.ext
theorem TopologicalSpace.Opens.ext :
∀ {α : Type u_2} [inst : TopologicalSpace α] {U V : TopologicalSpace.Opens α}, ↑U = ↑V → U = V
This theorem states that for any type `α` equipped with a topological space structure, and for any two open subsets `U` and `V` of this topological space, if the underlying set of `U` is equal to the underlying set of `V`, then `U` is equal to `V`. In simpler terms, two open subsets of a topological space are the same if they consist of the same set of points.
More concisely: In a topological space, two open sets with equal underlying sets are equal.
|
TopologicalSpace.OpenNhdsOf.mem
theorem TopologicalSpace.OpenNhdsOf.mem :
∀ {α : Type u_2} [inst : TopologicalSpace α] {x : α} (U : TopologicalSpace.OpenNhdsOf x), x ∈ U
This theorem states that for every open neighborhood `U` of a point `x` in a given topological space, `x` is always an element of `U`. Here, `α` is any type, which is equipped with the structure of a topological space. The `TopologicalSpace.OpenNhdsOf x` represents the collection of all open neighborhoods of `x`. The theorem ensures that any point is always contained within its own open neighborhoods in any topological space.
More concisely: For every point `x` in any topological space `α`, and every open neighborhood `U` of `x`, we have `x ∈ U`.
|
TopologicalSpace.Opens.is_open'
theorem TopologicalSpace.Opens.is_open' :
∀ {α : Type u_2} [inst : TopologicalSpace α] (self : TopologicalSpace.Opens α), IsOpen self.carrier
The theorem `TopologicalSpace.Opens.is_open'` states that for any type `α` that has a topological space structure, and for any element `self` from the `TopologicalSpace.Opens` of `α`, the `carrier` of `self` is an open set in that topological space. In other words, this theorem guarantees that the carrier set of any open subset of a topological space is itself an open set.
More concisely: For any topological space `α` and its open subset `self` from `TopologicalSpace.Opens α`, the carrier `self.carrier` is an open set in `α`.
|
TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion
theorem TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion :
∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Type u_5} (b : ι → TopologicalSpace.Opens α),
TopologicalSpace.Opens.IsBasis (Set.range b) →
(∀ (i : ι), IsCompact ↑(b i)) → ∀ (U : Set α), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑(b i)
This theorem states that for a topological space `α` and a function `b` mapping from some type `ι` to the open sets of `α`, if the range of `b` forms a basis for `α` where each element in the basis is a compact open set, then any open set `U` in `α` is compact if and only if `U` can be expressed as a finite union of some elements from the basis. Here `↑(b i)` denotes the open set corresponding to the `i`th element of the basis.
More concisely: A topological space's open set is compact if and only if it can be expressed as a finite union of compact open sets from a basis consisting of such sets.
|
TopologicalSpace.Opens.isOpen
theorem TopologicalSpace.Opens.isOpen :
∀ {α : Type u_2} [inst : TopologicalSpace α] (U : TopologicalSpace.Opens α), IsOpen ↑U
This theorem states that for any type `α` equipped with a topological space structure and any open set `U` in this topological space, `U` is indeed an open set in the ambient topological space on `α`. The theorem essentially confirms the fact that the elements of the structure `TopologicalSpace.Opens α`, which are supposed to represent open sets, are truly "open" according to the mathematics definition of openness in topology.
More concisely: For any topological space `(α, top)`, every element of `top.opens α` is an open set in `α`.
|
TopologicalSpace.Opens.mem_iSup
theorem TopologicalSpace.Opens.mem_iSup :
∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Sort u_5} {x : α} {s : ι → TopologicalSpace.Opens α},
x ∈ iSup s ↔ ∃ i, x ∈ s i
This theorem states that for any type `α` with a topology (`TopologicalSpace α`), any index type `ι`, any element `x` of `α`, and any mapping `s` from `ι` to the collection of open subsets of `α` (`TopologicalSpace.Opens α`), the element `x` belongs to the supremum of the indexed collection `s` if and only if there exists an index `i` such that `x` belongs to the open set `s i`. In simpler terms, a point is in the union of a collection of open sets if and only if it is in at least one of the open sets in the collection.
More concisely: For any topological space `α`, index type `ι`, and mapping `s` from `ι` to the opens of `α`, an element `x` in `α` lies in the supremum of `s` if and only if there exists an index `i` such that `x` is in `s i`. (Alternatively, `x` belongs to the union of the `s(i)` for some `i`.)
|
TopologicalSpace.Opens.coe_iSup
theorem TopologicalSpace.Opens.coe_iSup :
∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Sort u_5} (s : ι → TopologicalSpace.Opens α),
↑(⨆ i, s i) = ⋃ i, ↑(s i)
This theorem states that, for any topological space `α`, and any indexed set of open sets `s : ι → TopologicalSpace.Opens α`, the operation of taking the supremum (`⨆ i, s i`) in the lattice of open sets and then applying the coercion to sets (`↑`) is the same as first applying the coercion to each open set and then taking the union over all indices (`⋃ i, ↑(s i)`). In other words, in the context of topological spaces, the supremum of a collection of open sets, when viewed as a set, is the union of these sets.
More concisely: For any topological space `α` and indexed family `s : ι → OpenSet α`, the supremum of `s` in the lattice of open sets, as a set, equals the union of `{↑(s i) | i ∈ ι}`.
|
TopologicalSpace.Opens.coe_inj
theorem TopologicalSpace.Opens.coe_inj :
∀ {α : Type u_2} [inst : TopologicalSpace α] {U V : TopologicalSpace.Opens α}, ↑U = ↑V ↔ U = V
This theorem states that for any type `α` with a topological space structure, and any two members `U` and `V` of the open subsets of `α`, the assertion that the underlying sets of `U` and `V` are equal (denoted `↑U = ↑V`) is equivalent to `U` and `V` themselves being equal. In other words, two open subsets of a topological space are the same if and only if their underlying sets are the same.
More concisely: For any topological space `α`, two of its open subsets `U` and `V` are equal if and only if their underlying sets are equal (`↑U = ↑V` implies `U = V`).
|
TopologicalSpace.Opens.carrier_eq_coe
theorem TopologicalSpace.Opens.carrier_eq_coe :
∀ {α : Type u_2} [inst : TopologicalSpace α] (U : TopologicalSpace.Opens α), U.carrier = ↑U
This theorem states that for any given type `α` and any open subset `U` of a topological space over `α`, the carrier of `U` is equivalent to the coercion of `U`. In other words, the carrier of an open set in a topological space is the same as the set itself when we ignore the additional structure provided by the topology. The topology on `α` and the open set `U` are implicit arguments in this theorem.
More concisely: For any type `α` and open subset `U` of a topological space over `α`, the carrier of `U` is equal to the set `U` itself.
|
TopologicalSpace.OpenNhdsOf.mem'
theorem TopologicalSpace.OpenNhdsOf.mem' :
∀ {α : Type u_2} [inst : TopologicalSpace α] {x : α} (self : TopologicalSpace.OpenNhdsOf x), x ∈ self.carrier := by
sorry
This theorem states that for any given point `x` in a topological space `α`, the point `x` is an element of the carrier set of every open neighborhood `U` of `x`. In the language of topology, an open neighborhood of a point is a subset of the space that includes an open set containing the point, so this theorem is basically asserting that a point is always in its own neighborhood.
More concisely: For any point `x` in a topological space `α`, `x` belongs to every open neighborhood of `x`.
|
TopologicalSpace.Opens.coe_mk
theorem TopologicalSpace.Opens.coe_mk :
∀ {α : Type u_2} [inst : TopologicalSpace α] {U : Set α} {hU : IsOpen U}, ↑{ carrier := U, is_open' := hU } = U
This theorem in Lean 4 states that for any topological space `α`, any set `U` within `α`, and given that `U` is an open set, the coercion of the structured type `Opens α` (which includes `U` and the fact that `U` is open) to the type `Set α` is equivalent to `U` itself. In other words, when we have a structured type with a set and its property of being open, coercing it to its base set doesn't change the set: it still refers to the same collection of elements. This theorem is related to the concept of type coercion in Lean 4.
More concisely: For any topological space `α` and open set `U` within `α`, the coercion of the structured type `Opens α` containing `U` and its openness property to the type `Set α` is equal to `U`.
|