AlexandrovDiscrete.isOpen_sInter
theorem AlexandrovDiscrete.isOpen_sInter :
∀ {α : Type u_1} [inst : TopologicalSpace α] [self : AlexandrovDiscrete α] (S : Set (Set α)),
(∀ s ∈ S, IsOpen s) → IsOpen S.sInter
The theorem `AlexandrovDiscrete.isOpen_sInter` states that in an Alexandrov-discrete topological space, the intersection of an arbitrary collection of open sets is itself an open set. This is to say, given any type `α` with a topological space structure and an Alexandrov-discrete structure, and any collection `S` of subsets of `α` such that every subset `s` in `S` is open, the intersection of all sets in `S` is also an open set. This is a property of Alexandrov-discrete topological spaces, and is not generally true in arbitrary topological spaces. It's advised to use `isOpen_sInter` in the root namespace instead for this concept.
More concisely: In an Alexandrov-discrete topological space, the intersection of any collection of open sets is an open set.
|
exterior_def
theorem exterior_def :
∀ {α : Type u_3} [inst : TopologicalSpace α] (s : Set α), exterior s = {t | IsOpen t ∧ s ⊆ t}.sInter
The theorem `exterior_def` states that for all types `α` which have a topology, and for any set `s` of elements of type `α`, the exterior of `s` is equivalent to the intersection of all open sets `t` such that `s` is a subset of `t`. In other words, the exterior of a set `s` in a topological space is formed by intersecting all open sets which contain `s`.
More concisely: The exterior of a set in a topological space is equal to the intersection of all open sets that contain it.
|
isOpen_exterior
theorem isOpen_exterior :
∀ {α : Type u_3} [inst : TopologicalSpace α] {s : Set α} [inst_1 : AlexandrovDiscrete α], IsOpen (exterior s) := by
sorry
This theorem states that for any set `s` in a topological space `α`, if the topological space is Alexandrov-discrete, then the exterior of the set `s` is open. Here, the "exterior" of a set is defined as the intersection of all its neighborhoods, and a space is Alexandrov-discrete if every intersection of open sets is open. The assertion is that, under these conditions, the "exterior" of any set is always an open set.
More concisely: In an Alexandrov-discrete topological space, the exterior of any set is open.
|
alexandrovDiscrete_coinduced
theorem alexandrovDiscrete_coinduced :
∀ {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : AlexandrovDiscrete α] {β : Type u_5} {f : α → β},
AlexandrovDiscrete β
This theorem states that for any type `α` with a topological space structure and an Alexandrov discrete structure, and for any type `β` and any function from `α` to `β`, `β` has an Alexandrov discrete structure. In terms of mathematics, given a topological space `(α, τ)` that is Alexandrov discrete (i.e., any intersection of open sets is also open) and any function `f` from `α` to another set `β`, the topology on `β` induced by `f` is also Alexandrov discrete.
More concisely: Given a topological space `(α, τ)` that is Alexandrov discrete and a function `f : α → β`, the image `f(α)` under `f` inherits an Alexandrov discrete topology.
|
IsOpen.exterior_eq
theorem IsOpen.exterior_eq : ∀ {α : Type u_3} [inst : TopologicalSpace α] {s : Set α}, IsOpen s → exterior s = s := by
sorry
This theorem states that for any set `s` in a topological space `α`, if `s` is an open set, then the exterior of `s` is equal to `s` itself. In other words, for all open sets in a topological space, the intersection of all their neighborhoods (which is the definition of the exterior of a set) is the set itself. This theorem highlights a key property of open sets in a topological space.
More concisely: In a topological space, the exterior of an open set is equal to the set itself.
|
isOpen_sInter
theorem isOpen_sInter :
∀ {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : AlexandrovDiscrete α] {S : Set (Set α)},
(∀ s ∈ S, IsOpen s) → IsOpen S.sInter
The theorem `isOpen_sInter` states that for any type `α` equipped with a topological space structure and an Alexandrov discrete topology, if `S` is a set of subsets of `α` such that all subsets in `S` are open in `α`, then the intersection of all subsets in `S` (denoted by `⋂₀ S`) is also an open set in `α`.
More concisely: If `α` is a topological space with Alexandrov discrete topology and `S` is a non-empty family of open subsets of `α`, then their intersection is open in `α`.
|
subset_exterior
theorem subset_exterior : ∀ {α : Type u_3} [inst : TopologicalSpace α] {s : Set α}, s ⊆ exterior s
This theorem states that, for any set `s` within a topological space `α`, the set `s` is a subset of its exterior. In other words, every element in `s` is also in the exterior of `s`. This holds for all types `α` that have a topological space structure. In terms of topology, the "exterior" of a set is the intersection of all its neighborhoods, or in an Alexandrov-discrete space, it is the smallest neighborhood of the set. Therefore, this theorem asserts a fundamental property of set's exterior in the context of topology.
More concisely: In any topological space, every set is a subset of its exterior.
|
exterior_minimal
theorem exterior_minimal :
∀ {α : Type u_3} [inst : TopologicalSpace α] {s t : Set α}, s ⊆ t → IsOpen t → exterior s ⊆ t
The theorem `exterior_minimal` states that for any given type `α` in a topological space, and any two sets `s` and `t` of that type, if `s` is a subset of `t` and `t` is open in the topological space, then the exterior of `s` is a subset of `t`. In other words, the exterior of a set is the smallest open set that contains it. This captures the intuition that the "exterior" of a set includes all points that are not "immediately adjacent" to the set, in the sense of the given topology.
More concisely: For any topological space and types `α`, if `s` is a subset of open set `t`, then the exterior of `s` is contained in `t`.
|
isOpen_iInter
theorem isOpen_iInter :
∀ {ι : Sort u_1} {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : AlexandrovDiscrete α] {f : ι → Set α},
(∀ (i : ι), IsOpen (f i)) → IsOpen (⋂ i, f i)
The theorem `isOpen_iInter` states that for any index type `ι`, any type `α`, given a topological space over `α` and an Alexandrov discrete topology, and a function `f` from `ι` to the set of `α`, if each set `f i` is open for all `i` in `ι`, then the intersection of all such sets `f i` (denoted as `⋂ i, f i`) is also an open set. In other words, in an Alexandrov discrete topological space, the intersection of any collection of open sets is also an open set.
More concisely: In an Alexandrov discrete topological space, the intersection of any collection of open sets is open.
|