isGδ_biUnion
theorem isGδ_biUnion :
∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] {s : Set ι},
s.Finite → ∀ {f : ι → Set X}, (∀ i ∈ s, IsGδ (f i)) → IsGδ (⋃ i ∈ s, f i)
This theorem, termed as an alias of `IsGδ.biUnion`, states that the union of a finite number of Gδ sets is also a Gδ set. More formally, for any type `X` that is equipped with a topological space structure, a set `s` of type `ι`, and a function `f` from `ι` to sets of `X`, if the set `s` is finite and for every element `i` in `s`, the set `f(i)` is a Gδ set, then the union of the sets `f(i)` for all `i` in `s` is also a Gδ set. A Gδ set, to recall, is a countable intersection of open sets in a topological space.
More concisely: If `s` is a finite set and each `f(i)` is a Gδ set in a topological space `X`, then the union of `{f(i) | i ∈ s}` is also a Gδ set.
|
isGδ_sInter
theorem isGδ_sInter :
∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (Set X)}, (∀ s ∈ S, IsGδ s) → S.Countable → IsGδ S.sInter
This theorem, known as an alias of `IsGδ.sInter`, states that for any type `X` with a topological space structure, if you have a countable collection `S` of Gδ sets (which are countable intersections of open sets), then the countable intersection of all these Gδ sets is itself a Gδ set. In other words, if all sets `s` in `S` are Gδ sets and `S` itself is countable, then the set-theoretic intersection of all sets in `S` is also a Gδ set.
More concisely: If `X` is a topological space and `S` is a countable collection of Gδ sets in `X`, then the countable intersection of all sets in `S` is also a Gδ set.
|
IsMeagre.mono
theorem IsMeagre.mono : ∀ {X : Type u_5} [inst : TopologicalSpace X] {s t : Set X}, IsMeagre s → t ⊆ s → IsMeagre t
The theorem `IsMeagre.mono` states that for any type `X` that has a topological space structure, if a set `s` is meagre and another set `t` is a subset of `s`, then `t` is also meagre. In other words, in any given topological space, all subsets of a meagre set are themselves meagre.
More concisely: In any topological space, if a set is meagre then any subset of it is also meagre.
|
isGδ_setOf_continuousAt
theorem isGδ_setOf_continuousAt :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : UniformSpace Y]
[inst_2 : (uniformity Y).IsCountablyGenerated] (f : X → Y), IsGδ {x | ContinuousAt f x}
The theorem states that for any two types `X` and `Y`, where `X` is a topological space, `Y` is a uniform space and the uniformity on `Y` is countably generated, and for any function `f` from `X` to `Y`, the set of points in `X` at which `f` is continuous is a G-delta set. In mathematical terms, this means that the set of continuity points of any function from a topological space to a countably generated uniform space is a countable intersection of open sets.
More concisely: For any topological space X and countably generated uniform space Y, the set of continuity points of any function from X to Y forms a G-delta set.
|
IsGδ.biInter
theorem IsGδ.biInter :
∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] {s : Set ι},
s.Countable →
∀ {t : (i : ι) → i ∈ s → Set X}, (∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)) → IsGδ (⋂ i, ⋂ (h : i ∈ s), t i h)
The theorem `IsGδ.biInter` states that for any set `s` of type `ι` which is countable, if for every element `i` in `s` we have a corresponding G-delta set `t i hi` (where `hi` is proof that `i` is in `s`), then the intersection of all these G-delta sets is also a G-delta set. Here, a G-delta set in a topological space `X` is defined as a countable intersection of open sets in `X`. This theorem hence establishes the closure of G-delta sets under countable intersections. The set `s` indexes over the G-delta sets, and the theorem applies even when `s` is infinite, as long as it is countable.
More concisely: Given a countable set `s` of indices and for each `i` in `s`, a G-delta set `ti` in a topological space `X`, the intersection of all `ti` is also a G-delta set in `X`.
|
IsNowhereDense.subset_of_closed_isNowhereDense
theorem IsNowhereDense.subset_of_closed_isNowhereDense :
∀ {X : Type u_5} [inst : TopologicalSpace X] {s : Set X},
IsNowhereDense s → ∃ t, s ⊆ t ∧ IsNowhereDense t ∧ IsClosed t
The theorem `IsNowhereDense.subset_of_closed_isNowhereDense` states that for any nowhere dense set `s` in a topological space `X`, there exists a set `t` such that `s` is a subset of `t`, `t` is also nowhere dense, and `t` is closed. In other words, any nowhere dense set can be contained within a closed nowhere dense set, specifically its closure. In terms of topology, a set is nowhere dense if the interior of its closure is empty. This theorem helps in understanding the structure and properties of nowhere dense sets in the context of topological spaces.
More concisely: Given a nowhere dense set `s` in a topological space `X`, there exists a closed nowhere dense set `t` containing `s`.
|
mem_residual_iff
theorem mem_residual_iff :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
s ∈ residual X ↔ ∃ S, (∀ t ∈ S, IsOpen t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ S.sInter ⊆ s
This theorem states that a set is residual in a given topological space if and only if it includes a countable intersection of dense open sets. More specifically, for any topological space `X` and any set `s` in that space, `s` is in the residual of `X` if there exists another set `S` such that every element of `S` is both open and dense, `S` is countable, and the intersection of all elements in `S` is a subset of `s`.
More concisely: A set in a topological space is residual if and only if it intersects every countable intersection of dense open sets.
|
residual_of_dense_open
theorem residual_of_dense_open :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → Dense s → s ∈ residual X
This theorem states that in any given topological space `X`, if a set `s` is both open and dense, then it is also a residual set. In more mathematical terms, the theorem asserts that for all sets `s` in some topological space `X`, if `s` is an open set and every point in `X` belongs to the closure of `s` (i.e., `s` is dense), then `s` is included in a residual set of `X`, which is defined as a countable intersection of dense open sets.
More concisely: In any topological space, if a set is both open and dense, then it is a residual set.
|
meagre_empty
theorem meagre_empty : ∀ {X : Type u_5} [inst : TopologicalSpace X], IsMeagre ∅
The theorem `meagre_empty` states that for any type `X` that has a topological space structure, the empty set is meagre. In mathematical terms, this theorem says that the complement of the empty set, which is the entire space, is a residual (or comeagre) set in any topological space.
More concisely: In any topological space, the empty set is a meagre set, hence its complement is residual.
|
IsNowhereDense.closure
theorem IsNowhereDense.closure :
∀ {X : Type u_5} [inst : TopologicalSpace X] {s : Set X}, IsNowhereDense s → IsNowhereDense (closure s)
The theorem states that if a set `s` in a topological space `X` is nowhere dense, then its closure is also nowhere dense. Recall that a set is considered nowhere dense if its closure has an empty interior. Thus, the theorem essentially claims that the property of being nowhere dense is preserved under the operation of taking closures. In other words, the closure of a nowhere dense set is also a nowhere dense set.
More concisely: If a subset of a topological space is nowhere dense, then its closure also is nowhere dense.
|
IsOpen.isGδ
theorem IsOpen.isGδ : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → IsGδ s
This theorem states that any open set in a given topological space is a Gδ set. In the context of topology, a Gδ set is a countable intersection of open sets. Therefore, the theorem is saying that if a set is open in a topological space, then there exists a countable collection of open sets such that their intersection equals to the original set.
More concisely: In any topological space, every open set is a countable intersection of open sets (a Gδ set).
|
IsGδ.univ
theorem IsGδ.univ : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsGδ Set.univ
This theorem states that for any type `X` equipped with a topology (represented by `TopologicalSpace X`), the set of all elements of `X` (represented by `Set.univ`) is a Gδ set. In mathematical terminology, a Gδ set is a countable intersection of open sets. Therefore, the theorem asserts that the universal set in any topological space is a Gδ set, i.e., it can be represented as a countable intersection of open sets in that topology.
More concisely: In any topological space, the set of all points is a Gδ set, i.e., it is the countable intersection of open sets.
|
isNowhereDense_empty
theorem isNowhereDense_empty : ∀ {X : Type u_5} [inst : TopologicalSpace X], IsNowhereDense ∅
The theorem `isNowhereDense_empty` states that for every type `X` equipped with a topology (`TopologicalSpace X`), the empty set (`∅`) is nowhere dense. In mathematical terms, this means that the closure of the empty set is itself (which is still empty), and thus its interior is also empty. Therefore, the empty set satisfies the property of being "nowhere dense", which is defined as a set whose closure's interior is empty.
More concisely: The empty set is nowhere dense in any topological space.
|
IsGδ.eq_iInter_nat
theorem IsGδ.eq_iInter_nat :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsGδ s → ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ s = ⋂ n, f n
The theorem `IsGδ.eq_iInter_nat` states that for any set `s` in a given topological space `X`, if `s` is a Gδ set (a countable intersection of open sets), then there exists a sequence `f` of open sets such that `s` is the intersection of all sets in the sequence `f`. In other words, a Gδ set can be represented as an intersection of a sequence of open sets.
More concisely: A Gδ set in a topological space is equal to the intersection of a countable sequence of open sets.
|
IsClosed.isNowhereDense_iff
theorem IsClosed.isNowhereDense_iff :
∀ {X : Type u_5} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → (IsNowhereDense s ↔ interior s = ∅) := by
sorry
This theorem states that in any topological space `X`, for any set `s`, if `s` is a closed set then `s` is nowhere dense if and only if the interior of `s` is empty. In other words, within the context of a given topological space, a closed set is defined as being nowhere dense precisely when it has no interior points. Here, a set being "nowhere dense" means that the interior of its closure is empty, and the "interior" of a set is the largest open subset contained within it.
More concisely: In a topological space, a closed set is nowhere dense if and only if it has an empty interior.
|
isGδ_iInter
theorem isGδ_iInter :
∀ {X : Type u_1} {ι' : Sort u_4} [inst : TopologicalSpace X] [inst_1 : Countable ι'] {s : ι' → Set X},
(∀ (i : ι'), IsGδ (s i)) → IsGδ (⋂ i, s i)
This theorem, referred to as `isGδ_iInter`, states that the intersection of an encodable family of Gδ sets is itself a Gδ set.
A Gδ set, in a topological space, is defined as the countable intersection of open sets. Here, `X` represents the type of elements in our topological space, while `ι'` signifies an encodable (and hence countable) index set. The function `s : ι' → Set X` is a mapping from indices to Gδ sets in our space.
So, if for every index `i` in `ι'`, `s i` is a Gδ set, then the intersection of all these Gδ sets (expressed as `(⋂ i, s i)`) is also a Gδ set.
More concisely: If each `s i` is a Gδ set in a topological space, then their intersection `(⋂ i, s i)` is also a Gδ set.
|
residual_of_dense_Gδ
theorem residual_of_dense_Gδ :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsGδ s → Dense s → s ∈ residual X
The theorem states that in any topological space, if a set is both a Gδ set and dense, then it is residual. In other words, if a set is a countable intersection of open sets (Gδ set) and any point in the space is a limit point of this set (dense), then this set is a countable intersection of dense open sets (residual).
More concisely: In any topological space, a set that is both a Gδ set and dense is residual.
|
IsGδ.union
theorem IsGδ.union : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, IsGδ s → IsGδ t → IsGδ (s ∪ t) := by
sorry
This theorem states that the union of two Gδ sets is also a Gδ set. Here, a Gδ set in a topological space X is defined as a countable intersection of open sets. So, if we have two such Gδ sets `s` and `t` in the same topological space X, their union (denoted as `s ∪ t`) is guaranteed to also be a Gδ set.
More concisely: The union of two Gδ sets in a topological space is a Gδ set.
|
IsMeagre.inter
theorem IsMeagre.inter : ∀ {X : Type u_5} [inst : TopologicalSpace X] {s t : Set X}, IsMeagre s → IsMeagre (s ∩ t) := by
sorry
This theorem states that, given any topological space X and two sets s and t of X, if s is a meagre set, then the intersection of s and t is also a meagre set. In other words, intersecting a meagre set with any other set results in a set that is also meagre.
More concisely: If `s` is a meagre subset of a topological space `X`, then `s ∩ t` is also a meagre subset, for any subset `t` of `X`.
|
isMeagre_iff_countable_union_isNowhereDense
theorem isMeagre_iff_countable_union_isNowhereDense :
∀ {X : Type u_5} [inst : TopologicalSpace X] {s : Set X},
IsMeagre s ↔ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ S.sUnion
This theorem states that, in any topological space, a set is meagre if and only if it is contained in a countable union of nowhere dense sets. Here, a set is meagre if its complement is a residual set, and a set is nowhere dense if its closure has an empty interior. The theorem is expressed in the language of set theory, with the set being countable if it has the same cardinality as some subset of the natural numbers.
More concisely: A set is meagre in a topological space if and only if it is contained in a countable union of nowhere dense sets.
|
isClosed_isNowhereDense_iff_compl
theorem isClosed_isNowhereDense_iff_compl :
∀ {X : Type u_5} [inst : TopologicalSpace X] {s : Set X}, IsClosed s ∧ IsNowhereDense s ↔ IsOpen sᶜ ∧ Dense sᶜ := by
sorry
The theorem states that for any set `s` in a topological space `X`, the set `s` being closed and nowhere dense is equivalent to its complement `sᶜ` being open and dense. In other words, a set is closed (every limit point of the set is in the set) and nowhere dense (its closure's interior is empty) if and only if its complement is open (for every point in the set, there exists an open set containing that point and is completely contained in the set) and dense (every point in the space is either in the set or is a limit point of the set).
More concisely: A set is closed and nowhere dense if and only if its complement is open and dense.
|
isMeagre_iUnion
theorem isMeagre_iUnion :
∀ {X : Type u_5} [inst : TopologicalSpace X] {s : ℕ → Set X}, (∀ (n : ℕ), IsMeagre (s n)) → IsMeagre (⋃ n, s n)
This theorem states that in a given topological space `X`, if we have a sequence of sets `(s n)` such that every `s n` is a "meagre" set, then the countable union of all these sets is also a "meagre" set. In mathematical terms, a set is "meagre" if its complement is a residual (or comeagre) set.
More concisely: If every set in a countable sequence is meagre in a topological space X, then their countable union is also a meagre set. (In other words, the complement of the countable union is residual.)
|
IsGδ.iInter
theorem IsGδ.iInter :
∀ {X : Type u_1} {ι' : Sort u_4} [inst : TopologicalSpace X] [inst_1 : Countable ι'] {s : ι' → Set X},
(∀ (i : ι'), IsGδ (s i)) → IsGδ (⋂ i, s i)
This theorem states that the intersection of an encodable family of Gδ sets is also a Gδ set. In more detail, given any type `X` with a topological space structure, and an encodable sort `ι'`, if we have a function `s` from `ι'` to the sets of `X` such that each `s i` (for every `i` in `ι'`) is a Gδ set, then the intersection of all the `s i` is also a Gδ set. Remember, a Gδ set is defined as a countable intersection of open sets in the given topology.
More concisely: Given a topological space `X` and an encodable family `{s i | i ∈ ι'}` of Gδ sets, their intersection is also a Gδ set.
|