exists_subset_iUnion_closure_subset
theorem exists_subset_iUnion_closure_subset :
∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : NormalSpace X] {u : ι → Set X} {s : Set X},
IsClosed s →
(∀ (i : ι), IsOpen (u i)) →
(∀ x ∈ s, {i | x ∈ u i}.Finite) →
s ⊆ ⋃ i, u i → ∃ v, s ⊆ Set.iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
The **Shrinking Lemma** states that for any type `ι` and any type `X` with a topological space structure and a normal space structure, given a family `u` of sets of `X` indexed by `ι`, and a set `s` of `X`, if `s` is closed, each set `u(i)` for `i` in `ι` is open, for every element `x` in `s`, the set of indices `i` such that `x` belongs to `u(i)` is finite, and if `s` is a subset of the union of all `u(i)`, then there exists a family `v` of sets of `X` indexed by `ι` such that `s` is a subset of the indexed union of `v`, each `v(i)` for `i` in `ι` is open, and the closure of each `v(i)` is a subset of `u(i)`. In simple terms, it says that in a normal topological space, a point-finite open cover of a closed set can be refined to another open cover such that the closure of each new open set is contained in the corresponding original open set.
More concisely: In a normal topological space, a point-finite open cover of a closed set can be refined to another open cover with the property that the closure of each new open set is contained in the corresponding original open set.
|
ShrinkingLemma.PartialRefinement.apply_eq
theorem ShrinkingLemma.PartialRefinement.apply_eq :
∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X}
(self : ShrinkingLemma.PartialRefinement u s) {i : ι}, i ∉ self.carrier → self.toFun i = u i
The ShrinkingLemma.PartialRefinement.apply_eq theorem states that for any type `ι` and `X`, where `X` is a topological space, and any function `u : ι → Set X` mapping indices to sets in `X`, along with a set `s : Set X`, and a partial refinement `self` of `u` with respect to `s`, if an index `i` does not belong to the carrier of `self`, then applying `self.toFun` to `i` yields the same result as applying `u` to `i`. In simpler terms, sets that are not in the carrier of the partial refinement are left unchanged by the refinement process.
More concisely: For any topological space X, function u : ι -> Set X, set s : Set X, and partial refinement self of u with respect to s, if i is not in the carrier of self, then self.toFun i = u i.
|
exists_iUnion_eq_closed_subset
theorem exists_iUnion_eq_closed_subset :
∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : NormalSpace X] {u : ι → Set X},
(∀ (i : ι), IsOpen (u i)) →
(∀ (x : X), {i | x ∈ u i}.Finite) →
⋃ i, u i = Set.univ → ∃ v, Set.iUnion v = Set.univ ∧ (∀ (i : ι), IsClosed (v i)) ∧ ∀ (i : ι), v i ⊆ u i
This theorem is known as the Shrinking Lemma. It states that for any index set `ι`, and any topological space `X` that is a normal space, given a family `u : ι → Set X` of open sets in `X` such that every point in `X` is in a finite number of the sets `u i`, and the union of all the sets `u i` equals the universal set in `X`; there exists another family `v` of sets in `X` such that the union of all the sets `v i` also equals the universal set, and each `v i` is a closed set and is a subset of the corresponding `u i`. The lemma essentially asserts that a point-finite open cover of a closed subset of a normal space can be "shrunk" to a new closed cover where each of the new closed sets is contained within the corresponding original open set.
More concisely: Given a normal space `X` and a point-finite open cover `u : ι → Set X` of a closed subset with union equal to `X`, there exists a closed cover `v : ι → Set X` such that each `v i` is a subset of `ui`.
|
ShrinkingLemma.PartialRefinement.apply_eq_of_chain
theorem ShrinkingLemma.PartialRefinement.apply_eq_of_chain :
∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X}
{c : Set (ShrinkingLemma.PartialRefinement u s)},
IsChain (fun x x_1 => x ≤ x_1) c →
∀ {v₁ v₂ : ShrinkingLemma.PartialRefinement u s},
v₁ ∈ c → v₂ ∈ c → ∀ {i : ι}, i ∈ v₁.carrier → i ∈ v₂.carrier → v₁.toFun i = v₂.toFun i
The theorem, `ShrinkingLemma.PartialRefinement.apply_eq_of_chain`, states that if we have two partial refinements, `v₁` and `v₂`, that are elements of a chain (which means they are comparable), and an index `i` that is in the carriers of both these partial refinements, then the function application of `v₁` at `i` is equal to the function application of `v₂` at `i`. This is stated in the context of a topological space `X` indexed by `ι`, a set function `u : ι → Set X`, and a set `s : Set X`. The chain is a set of partial refinements of `u` and `s`, and is ordered by the partial order `≤`.
More concisely: If `v₁` and `v₂` are comparable partial refinements in a chain of set functions `u : ι → X` and `s : Set X`, and `i` is in the carrier of both, then `v₁ i = v₂ i`.
|
ShrinkingLemma.PartialRefinement.subset_iUnion
theorem ShrinkingLemma.PartialRefinement.subset_iUnion :
∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X}
(self : ShrinkingLemma.PartialRefinement u s), s ⊆ ⋃ i, self.toFun i
This theorem, known as the Shrinking Lemma, asserts that for any types `ι` and `X` with `X` equipped with a topological space structure, and any functions `u` mapping from `ι` to a set of `X` and `s` representing a set of `X`, the partially refined family, as defined by `self` which is a partial refinement of `u` on `s`, still covers the set `s`. In mathematical terms, it means that the set `s` is a subset of the union over all `i` of `self.toFun i`, where `self.toFun` is the function represented by the partial refinement `self`.
More concisely: For any type `X` with a topological space structure, any function `u` from a type `ι` to `X`, and any set `s` in `X`, the partially refined family `self` of `u` on `s` covers `s`, i.e., `s` is a subset of the union of `self.toFun i` over all `i` in `ι`.
|
exists_iUnion_eq_closure_subset
theorem exists_iUnion_eq_closure_subset :
∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : NormalSpace X] {u : ι → Set X},
(∀ (i : ι), IsOpen (u i)) →
(∀ (x : X), {i | x ∈ u i}.Finite) →
⋃ i, u i = Set.univ →
∃ v, Set.iUnion v = Set.univ ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
This theorem, often referred to as the "Shrinking Lemma", states that for any indexed set of subsets of a topological space (where this topological space is normal), if each subset is open and every point in the space belongs to only finitely many of these subsets (point-finite), and if the union of all these subsets is the whole space, then there exists a new indexed set of open subsets such that their union also forms the whole space and the closure of each new open set is contained in the corresponding original open set. Essentially, it provides a way to "shrink" an open cover of a closed subset of a normal space to a new open cover with the same union, but with the extra property that the closure of each new open set lies within its original counterpart. This theorem is important in the study of topological spaces and their properties.
More concisely: In a normal topological space, given an indexed family of open subsets with finitely many sets containing any point and whose union is the whole space, there exists an open refinement with the same union whose closure is contained in each original set.
|
ShrinkingLemma.PartialRefinement.le_chainSup
theorem ShrinkingLemma.PartialRefinement.le_chainSup :
∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X}
{c : Set (ShrinkingLemma.PartialRefinement u s)} (hc : IsChain (fun x x_1 => x ≤ x_1) c) (ne : c.Nonempty)
(hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite) (hU : s ⊆ ⋃ i, u i) {v : ShrinkingLemma.PartialRefinement u s},
v ∈ c → v ≤ ShrinkingLemma.PartialRefinement.chainSup c hc ne hfin hU
The theorem `ShrinkingLemma.PartialRefinement.le_chainSup` states that for any set `s` of type `X`, where `X` is a topological space, and a family of sets `u` indexed by type `ι`, if a set `c` of partial refinements on `u` and `s` forms a chain (i.e., for any two elements in the set, one is less than or equal to the other), and the set `c` is nonempty, and for every element in `s`, the set of indices `i` for which the element belongs to `u[i]` is finite, and `s` is a subset of the union of the sets `u[i]` for all `i`, then any partial refinement `v` in `c` is less than or equal to the supremum of the chain `c`. In context, this theorem is used to establish a property about refinement of open covers in topological spaces.
More concisely: If `s` is a subset of a topological space `X`, `u` is a family of sets indexed by type `ι`, `c` is a nonempty chain of partial refinements of `s` by `u`, and for every element in `s`, the set of indices `i` for which it belongs to `u[i]` is finite, then any `v` in `c` is less than or equal to the supremum of `c`.
|
exists_subset_iUnion_closed_subset
theorem exists_subset_iUnion_closed_subset :
∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : NormalSpace X] {u : ι → Set X} {s : Set X},
IsClosed s →
(∀ (i : ι), IsOpen (u i)) →
(∀ x ∈ s, {i | x ∈ u i}.Finite) →
s ⊆ ⋃ i, u i → ∃ v, s ⊆ Set.iUnion v ∧ (∀ (i : ι), IsClosed (v i)) ∧ ∀ (i : ι), v i ⊆ u i
The **Shrinking Lemma** states that given a normal topological space `X`, an indexed collection `u` of open sets in `X`, and a closed set `s` in `X`, if every point in `s` is contained in a finite number of sets from the collection `u` (making `u` a point-finite open cover of `s`), and `s` is a subset of the union of the sets in `u`, then there exists a new indexed collection `v` of sets such that: `s` is a subset of the union of the sets in `v`; each set in `v` is closed; and each set in `v` is a subset of the corresponding set in `u`. This means we can "shrink" the open cover `u` to a closed cover `v` such that each new closed set is contained in the corresponding original open set.
More concisely: Given a normal topological space, a point-finite open cover, and a closed subset lying in the cover's union, there exists a closed subcover with the same union.
|
ShrinkingLemma.PartialRefinement.mem_find_carrier_iff
theorem ShrinkingLemma.PartialRefinement.mem_find_carrier_iff :
∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X}
{c : Set (ShrinkingLemma.PartialRefinement u s)} {i : ι} (ne : c.Nonempty),
i ∈ (ShrinkingLemma.PartialRefinement.find c ne i).carrier ↔
i ∈ ShrinkingLemma.PartialRefinement.chainSupCarrier c
This theorem, `ShrinkingLemma.PartialRefinement.mem_find_carrier_iff`, states that for a given nonempty set of partial refinements `c` of some topology `X` indexed by type `ι`, and a given `ι` index `i`, the index `i` is in the carrier of the partial refinement selected by the `find` function if and only if `i` is in the carrier of the least upper bound of the chain of these partial refinements. In simpler terms, it says that the `find` function will locate a partial refinement in the chain that contains the index `i`, if and only if `i` is included in the union of all the carriers in the chain.
More concisely: For a nonempty chain of partial refinements of a topology, an index is in the carrier of the partial refinement selected by `find` if and only if it is in the carrier of their least upper bound.
|
ShrinkingLemma.PartialRefinement.exists_gt
theorem ShrinkingLemma.PartialRefinement.exists_gt :
∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : NormalSpace X] {u : ι → Set X} {s : Set X}
(v : ShrinkingLemma.PartialRefinement u s), IsClosed s → ∀ i ∉ v.carrier, ∃ v', v < v'
The theorem `ShrinkingLemma.PartialRefinement.exists_gt` states that for any topological space `X` with normality condition, any given set `s` in `X` that is closed, any function `u` from an index set `ι` to the set of subsets of `X`, and any partial refinement `v` of `u` (in respect to `s`), if there exists an index `i` that is not in the carrier of `v`, then there exists another partial refinement `v'` which is strictly greater than `v`. In other words, we can always find a stricter partial refinement if our current refinement doesn't cover all indices.
More concisely: For any closed set `s` in a normality topological space `X`, if `u` is a function from an index set `ι` to the power set of `X`, and `v` is a partial refinement of `u` with respect to `s` such that the carrier of `v` does not contain all indices in `ι`, then there exists a strict partial refinement `v'` of `u` with respect to `s`.
|
ShrinkingLemma.PartialRefinement.isOpen
theorem ShrinkingLemma.PartialRefinement.isOpen :
∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X}
(self : ShrinkingLemma.PartialRefinement u s) (i : ι), IsOpen (self.toFun i)
The theorem `ShrinkingLemma.PartialRefinement.isOpen` states that for any type `ι`, any topological space `X`, any function `u` from `ι` to the set of points in `X`, and any set `s` in `X`, if we have a partial refinement `self` of `s` with respect to `u`, then the image of any element `i` of `ι` under the function represented by `self` is an open set in the topological space `X`. Here, a partial refinement is a concept from the Shrinking Lemma in topology, which is a procedure used to refine open covers of topological spaces.
More concisely: Given a type ι, a topological space X, a function u from ι to X, and a partial refinement self of a set s in X with respect to u, the image of each i in ι under self is an open set in X.
|
ShrinkingLemma.PartialRefinement.closure_subset
theorem ShrinkingLemma.PartialRefinement.closure_subset :
∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X}
(self : ShrinkingLemma.PartialRefinement u s) {i : ι}, i ∈ self.carrier → closure (self.toFun i) ⊆ u i
The theorem `ShrinkingLemma.PartialRefinement.closure_subset` states that for any type `ι` and any topological space `X`, if we have a function `u` from `ι` to the set of `X`, and a set `s` of `X`, and a partial refinement `self` of `s` with respect to `u`, then for any element `i` of the carrier of `self`, the closure of the set corresponding to `i` under the function represented by `self` is a subset of the set `u i`. In simpler terms, this means that the closure of each set in the refined collection is still contained within the corresponding set in the original collection.
More concisely: For any type `ι`, topological space `X`, function `u` from `ι` to `X`, set `s`, and partial refinement `self` of `s` with respect to `u`, the closure of each set in the refined collection is contained in the corresponding set in the original collection, i.e., for all `i` in the carrier of `self`, the closure of `u i` from `self` is a subset of `u i` in `X`.
|