Dense.inter_of_Gδ
theorem Dense.inter_of_Gδ :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {s t : Set X},
IsGδ s → IsGδ t → Dense s → Dense t → Dense (s ∩ t)
The Baire theorem states that in any given Baire space, which is a specific kind of topological space, the intersection of two Gδ sets that are both dense will also be a dense set. Here, a Gδ set is defined as a countable intersection of open sets, and a set is said to be dense if every point in the space belongs to its closure.
More concisely: In a Baire space, the intersection of two Gδ sets that are dense is also dense.
|
dense_iInter_of_isOpen
theorem dense_iInter_of_isOpen :
∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] [inst_2 : Countable ι]
{f : ι → Set X}, (∀ (i : ι), IsOpen (f i)) → (∀ (i : ι), Dense (f i)) → Dense (⋂ s, f s)
The theorem `dense_iInter_of_isOpen` is a formal statement of the Baire Category Theorem in the context of a topological space. In more detail, it states that given a topological space `X` which is also a Baire space and `ι` a countable index set, for any family of sets `f : ι → Set X`, where each `f i` is both open and dense in `X`, the countable intersection of these sets (denoted as `⋂ s, f s`) is also dense in `X`. In essence, this theorem says that in a Baire space, the intersection of countably many open and dense sets remains dense.
More concisely: In a Baire space, the countable intersection of countably many open and dense sets is dense.
|
dense_sInter_of_Gδ
theorem dense_sInter_of_Gδ :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {S : Set (Set X)},
(∀ s ∈ S, IsGδ s) → S.Countable → (∀ s ∈ S, Dense s) → Dense S.sInter
The Baire theorem is a statement about topological spaces and sets within these spaces. Specifically, the theorem states that in a Baire space - a type of topological space, the countable intersection of dense Gδ sets is also a dense set. Here, a Gδ set is defined as a countable intersection of open sets, and a set is called dense if every point in the topological space belongs to its closure. The closure of a set includes all the points of the set itself, as well as any limit points. The theorem is formulated here with the symbol ⋂₀, which denotes the intersection of all sets in a collection.
More concisely: In a Baire space, the countable intersection of dense Gδ sets is a dense set.
|
dense_biUnion_interior_of_closed
theorem dense_biUnion_interior_of_closed :
∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {S : Set α} {f : α → Set X},
(∀ s ∈ S, IsClosed (f s)) → S.Countable → ⋃ s ∈ S, f s = Set.univ → Dense (⋃ s ∈ S, interior (f s))
This theorem, often referred to as Baire's Theorem, states that if a topological space is a Baire space (a space in which the intersection of countably many dense open sets is dense), and if we have a countable set of closed sets (indexed by any type α) that cover this whole space, then the interiors of these closed sets are dense. In other words, every point in the space is a point of closure of the set formed by the interiors. This theorem is a key result in general topology and has significant applications in analysis.
More concisely: In a Baire space, the intersection of the interiors of a countable collection of closed sets is dense.
|
dense_sUnion_interior_of_closed
theorem dense_sUnion_interior_of_closed :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {S : Set (Set X)},
(∀ s ∈ S, IsClosed s) → S.Countable → S.sUnion = Set.univ → Dense (⋃ s ∈ S, interior s)
The theorem `dense_sUnion_interior_of_closed` is also known as the Baire theorem. In the context of topology, it states that for a Baire space `X`, if we have a countable collection `S` of closed sets such that their union covers the whole space (i.e., it is equal to the universal set), then the union of the interiors of these sets is dense in `X`. In other words, any point in `X` is either in the union of the interiors or can be approximated by points from it. This theorem is a fundamental result in topology and analysis, assuring that countable intersections of dense open sets are still dense.
More concisely: In a Baire space, the union of the interiors of a countable collection of closed sets covers the whole space implies that any point is in the union or is approximated by it.
|
dense_biInter_of_Gδ
theorem dense_biInter_of_Gδ :
∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {S : Set α}
{f : (x : α) → x ∈ S → Set X},
(∀ (s : α) (H : s ∈ S), IsGδ (f s H)) →
S.Countable → (∀ (s : α) (H : s ∈ S), Dense (f s H)) → Dense (⋂ s, ⋂ (h : s ∈ S), f s h)
This theorem, known as the Baire theorem, states that in any given topological space (that is also a Baire space), the countable intersection of dense Gδ sets is also dense. Here, a Gδ set is defined as a countable intersection of open sets, and a set is considered dense in a topological space if every point belongs to its closure. The theorem is formulated with an index set which can be any countable set. Specifically, for all sets `S` of elements of type `α`, and a function `f` that maps each element of `S` to a set in the topological space `X`, if each set `f s H` (for `s` in `S` and `H` a proof that `s` is in `S`) is a Gδ set and is dense, then the intersection of all such sets is also dense.
More concisely: In a Baire space, the countable intersection of dense Gδ sets is dense.
|
nonempty_interior_of_iUnion_of_closed
theorem nonempty_interior_of_iUnion_of_closed :
∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] [inst_2 : Nonempty X]
[inst_3 : Countable ι] {f : ι → Set X},
(∀ (i : ι), IsClosed (f i)) → ⋃ i, f i = Set.univ → ∃ i, (interior (f i)).Nonempty
This theorem, named "nonempty_interior_of_iUnion_of_closed," is a helpful result derived from Baire's theorem. It states that for any type `X` endowed with a topological space structure, Baire space structure, and an assurance that `X` is nonempty, along with a countable index type `ι`, if a collection of sets `f` indexed by `ι` is such that each `f i` is closed, and the union of all these sets equals the universal set (i.e., it covers the entire space `X`), then there exists at least one index `i` such that the interior of the set `f i` is not empty. This essentially means under these conditions, at least one of these closed sets must have a "nonempty interior," or in other words, contain a nonempty open set within it.
More concisely: If `X` is a nonempty topological space, and `{fi : ι → set X} | ∀i, fi is closed` such that `⋃i, fi = X`, then there exists an `i` such that `int (fi i) ≠ ∅`.
|
dense_iInter_of_Gδ
theorem dense_iInter_of_Gδ :
∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] [inst_2 : Countable ι]
{f : ι → Set X}, (∀ (s : ι), IsGδ (f s)) → (∀ (s : ι), Dense (f s)) → Dense (⋂ s, f s)
The Baire's theorem states that in a topological space that is also a Baire space, given a countable set of indices, if for each index from this set, the corresponding set is a Gδ set (a countable intersection of open sets) and is dense (every point in the space belongs to its closure), then the intersection of all these sets is also dense. This theorem is formulated here with an index set which is a countable type.
More concisely: In a Baire space, the intersection of a countable family of dense Gδ sets is dense.
|
dense_iInter_of_isOpen_nat
theorem dense_iInter_of_isOpen_nat :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {f : ℕ → Set X},
(∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)
This theorem defines a property of a Baire space. Given a type `X` with a topological space structure and a Baire space structure, and a function `f` from natural numbers to sets of `X`, if for every natural number `n`, the set `f n` is open in the topological space and is also dense, then the intersection of all these sets (denoted by `⋂ n, f n`) is also a dense set in the topological space. In other words, in a Baire space, the countable intersection of dense open sets remains dense.
More concisely: In a Baire space, the countable intersection of dense open sets is dense.
|
mem_residual
theorem mem_residual :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {s : Set X},
s ∈ residual X ↔ ∃ t ⊆ s, IsGδ t ∧ Dense t
This theorem states that for any set `s` in a type `X` with a topological space and Baire space structure, `s` is considered residual, or comeagre, if and only if there exists a subset `t` of `s` that is both a Gδ set and dense. A Gδ set is a countable intersection of open sets, and a set is said to be dense if every point belongs to its closure. The Baire space structure implies that the intersection of countably many dense open sets is not empty.
More concisely: A subset of a topological space with a Baire space structure is residual if and only if it is the intersection of a countable number of dense open sets (i.e., a Gδ dense set).
|
IsGδ.dense_biUnion_interior_of_closed
theorem IsGδ.dense_biUnion_interior_of_closed :
∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {t : Set α} {s : Set X},
IsGδ s →
Dense s →
t.Countable →
∀ {f : α → Set X}, (∀ i ∈ t, IsClosed (f i)) → s ⊆ ⋃ i ∈ t, f i → Dense (⋃ i ∈ t, interior (f i))
The theorem `IsGδ.dense_biUnion_interior_of_closed` states that in a Baire Space (a type of topological space), given a dense G-delta set and a countable family of closed sets that cover this G-delta set, the union of the interiors of the closed sets is also a dense set.
In more detail, consider a dense G-delta set `s` in a Baire Space `X`. Suppose we have a countable set `t` and for each element `i` in `t`, we associate a closed set `f i` such that `s` is a subset of the union of these `f i`. Then the theorem asserts that the union of the interiors of these closed sets `f i` forms a dense set in the space `X`.
More concisely: In a Baire Space, if a dense G-delta set is covered by a countable family of closed sets, then the union of their interiors is also a dense set.
|
IsGδ.dense_sUnion_interior_of_closed
theorem IsGδ.dense_sUnion_interior_of_closed :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {T : Set (Set X)} {s : Set X},
IsGδ s → Dense s → T.Countable → (∀ t ∈ T, IsClosed t) → s ⊆ T.sUnion → Dense (⋃ t ∈ T, interior t)
In the context of a topological space, this theorem states that if a countable family of closed sets cover a dense Gδ set, then the union of their interiors is also dense. More formally, given a type `X`, a topological space over `X`, a Baire space instance for `X`, a set `T` of subsets of `X`, and a subset `s` of `X`, if `s` is a Gδ set and is also dense, `T` is countable, every set in `T` is closed, and `s` is a subset of the union of the sets in `T`, then the interior of each set in `T` forms a collection of subsets whose union is a dense set. This theorem demonstrates a property about the interaction of dense sets, countability, and interior sets in the framework of topological and Baire spaces.
More concisely: If a countable family of closed sets covers a dense Gδ set in a topological Baire space, then the union of their interiors is also dense.
|
dense_iUnion_interior_of_closed
theorem dense_iUnion_interior_of_closed :
∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] [inst_2 : Countable ι]
{f : ι → Set X}, (∀ (i : ι), IsClosed (f i)) → ⋃ i, f i = Set.univ → Dense (⋃ i, interior (f i))
The theorem named `dense_iUnion_interior_of_closed` is a formulation of the Baire theorem in the context of topology. It states that for any type `X`, equipped with a topological space structure, and any countable type `ι`, if we have a function `f` from `ι` to the set of subsets of `X`, such that each set `f i` (for `i` in `ι`) is a closed set, and the union over all these sets `f i` equals the universal set (i.e., the entire space `X`), then the union of the interiors of all these sets `f i` is a dense set in `X`. Here, a set is considered dense if every point in `X` belongs to its closure, and the interior of a set is the largest open subset of that set. This theorem is applicable in the context of a Baire space, which is a complete metric space that satisfies a certain property related to the intersection of dense open sets.
More concisely: In a Baire space, the union of the interiors of any countable collection of closed sets that cover the entire space is dense.
|
IsGδ.dense_iUnion_interior_of_closed
theorem IsGδ.dense_iUnion_interior_of_closed :
∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] [inst_2 : Countable ι]
{s : Set X},
IsGδ s → Dense s → ∀ {f : ι → Set X}, (∀ (i : ι), IsClosed (f i)) → s ⊆ ⋃ i, f i → Dense (⋃ i, interior (f i))
The theorem `IsGδ.dense_iUnion_interior_of_closed` states that in a topological space endowed with a Baire property, if a countable family of closed sets covers a dense Gδ set, then the union of the interiors of these closed sets is also a dense set. Here, a Gδ set is defined as a countable intersection of open sets, a set is dense if every point belongs to its closure, and the interior of a set is the largest open subset of the set. The union operation is denoted by `⋃`.
More concisely: In a Baire topological space, if a countable family of closed sets covers a dense Gδ set, then the interior of their union equals the dense Gδ set.
|
dense_biInter_of_isOpen
theorem dense_biInter_of_isOpen :
∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {S : Set α} {f : α → Set X},
(∀ s ∈ S, IsOpen (f s)) → S.Countable → (∀ s ∈ S, Dense (f s)) → Dense (⋂ s ∈ S, f s)
This theorem is a version of the Baire's theorem in topology. It states that given a topological space `X`, a Baire space `X`, a set `S` of any type `α`, and a function `f` mapping from `α` to a set of `X`, if every `f(s)` for `s` in `S` is an open set and is dense in `X`, and if the set `S` is countable, then the countable intersection of all `f(s)` for `s` in `S`, denoted as `(⋂ s ∈ S, f s)`, is also a dense set in `X`. In other words, a countable intersection of dense open sets in a Baire space remains dense.
More concisely: In a Baire space, the countable intersection of any countable family of dense open sets is dense.
|
eventually_residual
theorem eventually_residual :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {p : X → Prop},
(∀ᶠ (x : X) in residual X, p x) ↔ ∃ t, IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
The theorem `eventually_residual` states that for any topological space `X` which also satisfies the property of being a Baire space, a property `p` holds for all elements in a residual set (also known as a comeagre set, i.e., a countable intersection of dense open sets) if and only if there exists a set `t` such that `t` is a Gδ set (i.e., a countable intersection of open sets), `t` is dense, and the property `p` holds for all elements in `t`.
More concisely: In a Baire space X, a property holds for almost all elements if and only if it holds for all elements in a Gδ set where the Gδ set is dense in X.
|
dense_sInter_of_isOpen
theorem dense_sInter_of_isOpen :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {S : Set (Set X)},
(∀ s ∈ S, IsOpen s) → S.Countable → (∀ s ∈ S, Dense s) → Dense S.sInter
The Baire theorem states that, for any topological space `X` that is also a Baire space, the countable intersection of dense open sets is dense. More formally, given a set `S` of sets of type `X`, if every `s` in `S` is open and dense, and `S` is countable, then the intersection of all sets in `S` (denoted by `⋂₀ S` in Lean) is also a dense set.
More concisely: In a Baire space, the countable intersection of dense open sets is dense.
|