TopologicalSpace.isOpen_univ
theorem TopologicalSpace.isOpen_univ : ∀ {X : Type u} [self : TopologicalSpace X], TopologicalSpace.IsOpen Set.univ
This theorem states that the set representing the entire space is an open set. In more detail, for any type `X` that has a topological space structure, the universal set of `X` (which contains all elements of `X`) is considered an open set within this topological space. In mathematical terms, this is expressing the fact that in topology, the set containing all points in a given space is defined to be an open set. The theorem is referred to as `isOpen_univ` in the root namespace.
More concisely: In any topological space, the universal set is an open set.
|
Mathlib.Topology.Defs.Basic._auxLemma.1
theorem Mathlib.Topology.Defs.Basic._auxLemma.1 : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpen Set.univ = True
The theorem `Mathlib.Topology.Defs.Basic._auxLemma.1` states that for any type `X` that has a topological space structure, the universal set of `X` is an open set. In mathematical terms, this theorem asserts that the entire set in any given topological space is always an open set. This is a fundamental property in topology, where the entire space and the empty set are considered open by definition.
More concisely: In any topological space, the universal set is open.
|
isOpen_sUnion
theorem isOpen_sUnion :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set (Set X)}, (∀ t ∈ s, IsOpen t) → IsOpen s.sUnion
The theorem `isOpen_sUnion` states that for any type `X` with a topological space structure and a set `s` of subsets of `X`, if all the subsets contained in `s` are open in the topological space, then the union of all subsets in `s` (denoted as `⋃₀ s`) is also open in the same topological space. In more mathematical language, given a set `s` of open subsets of a topological space `X`, the union of the elements of `s` is also an open set in `X`.
More concisely: If every subset in a collection of open subsets of a topological space is open, then their union is also open.
|
IsOpen.inter
theorem IsOpen.inter : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsOpen s → IsOpen t → IsOpen (s ∩ t)
This theorem specifies that for any type `X` equipped with a topological space structure, if `s` and `t` are sets of elements of type `X` and both `s` and `t` are open in this topological space, then the intersection of `s` and `t` is also open in the topological space. In the language of topology, this theorem states that the intersection of any two open sets is also open, a fundamental property of topological spaces.
More concisely: In any topological space, the intersection of two open sets is open.
|
isOpen_univ
theorem isOpen_univ : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpen Set.univ
The theorem `isOpen_univ` states that for any type `X` that has a topological space structure, the universal set on `X` is open in the corresponding topological space. In other words, the set of all elements of `X` is an open set, as per the definition of openness in the given topological space on `X`. This is a universal property, valid for any topological space.
More concisely: The universal set of any topological space is open in that space.
|
TopologicalSpace.isOpen_sUnion
theorem TopologicalSpace.isOpen_sUnion :
∀ {X : Type u} [self : TopologicalSpace X] (s : Set (Set X)),
(∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen s.sUnion
This theorem states that in any topological space `X`, if we have a collection `s` of subsets of `X`, where each subset is an open set, then the union of all subsets in this collection (denoted as `s.sUnion`) is also an open set. In other words, in the context of topology, the union of a family of open sets remains open.
More concisely: In any topological space, the union of a collection of open sets is an open set.
|
IsClosed.isOpen_compl
theorem IsClosed.isOpen_compl : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [self : IsClosed s], IsOpen sᶜ
This theorem states that the complement of a closed set is an open set in a given topological space. More formally, for any type `X` equipped with a topology (represented by `inst : TopologicalSpace X`) and any set `s` of type `X` that is closed (denoted by `self : IsClosed s`), the complement of `s` (denoted by `sᶜ`) is an open set. This is a fundamental concept in topology.
More concisely: The complement of a closed set is an open set in a topological space.
|
TopologicalSpace.isOpen_inter
theorem TopologicalSpace.isOpen_inter :
∀ {X : Type u} [self : TopologicalSpace X] (s t : Set X),
TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
The theorem `TopologicalSpace.isOpen_inter` asserts that in any topological space `X`, the intersection of two open sets `s` and `t` is also an open set. That is, if `s` and `t` are open sets in `X`, then the set `s ∩ t` is also an open set in `X`. The function `TopologicalSpace.IsOpen` is used to express the openness of a set within a given topological space. The official function to use for this assertion is `IsOpen.inter`.
More concisely: In a topological space, the intersection of any two open sets is an open set.
|
Continuous.isOpen_preimage
theorem Continuous.isOpen_preimage :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
Continuous f → ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)
The theorem, `Continuous.isOpen_preimage`, states that for any types `X` and `Y` endowed with topological spaces, any continuous function `f` from `X` to `Y`, and any open set `s` in `Y`, the preimage of `s` under `f` is an open set in `X`. In other words, if you have a continuous function and an open set in the codomain, then the set of all points in the domain that map to this open set is also open. This is one of the key properties that defines a continuous function in topology.
More concisely: If `f:` X -> Y is continuous and `s` is open in Y, then `f^(-1)(s)` is open in X.
|