irreducibleComponent_property
theorem irreducibleComponent_property :
∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X),
IsPreirreducible (irreducibleComponent x) ∧
{x} ⊆ irreducibleComponent x ∧
∀ (u : Set X), IsPreirreducible u → irreducibleComponent x ⊆ u → u = irreducibleComponent x
The theorem `irreducibleComponent_property` asserts that for every topological space `X` and any point `x` in `X`, the irreducible component containing `x` has three properties. First, it is a pre-irreducible set. In other words, if we take any two open sets `u` and `v` that both have a non-empty intersection with the irreducible component, then the intersection of the irreducible component with the intersection of `u` and `v` is also non-empty. Second, the singleton set containing `x` is a subset of the irreducible component. Finally, the irreducible component is maximal among the pre-irreducible sets containing `x`: if `u` is any pre-irreducible set that contains the irreducible component, then `u` must in fact be equal to the irreducible component.
More concisely: For every point `x` in a topological space `X`, the irreducible component containing `x` is a maximal pre-irreducible set that contains `x` and is a subset of every pre-irreducible set that contains it.
|
subset_closure_inter_of_isPreirreducible_of_isOpen
theorem subset_closure_inter_of_isPreirreducible_of_isOpen :
∀ {X : Type u_1} [inst : TopologicalSpace X] {S U : Set X},
IsPreirreducible S → IsOpen U → (S ∩ U).Nonempty → S ⊆ closure (S ∩ U)
The theorem `subset_closure_inter_of_isPreirreducible_of_isOpen` states that for any topological space `X` and any subsets `S` and `U` of `X`, if `S` is preirreducible, `U` is open, and the intersection of `S` and `U` is nonempty, then `S` is a subset of the closure of the intersection of `S` and `U`. In other words, in a topological space, a nonempty open subset of a preirreducible subspace is dense in the subspace.
More concisely: If a preirreducible subset of a topological space is non-empty and intersects an open subset, then the preirreducible subset is a subset of the closure of their intersection.
|
IsPreirreducible.subset_irreducible
theorem IsPreirreducible.subset_irreducible :
∀ {X : Type u_1} [inst : TopologicalSpace X] {t S U : Set X},
IsPreirreducible t → U.Nonempty → IsOpen U → U ⊆ S → S ⊆ t → IsIrreducible S
This theorem states that, for any type `X` equipped with a topology, if `t`, `S`, and `U` are sets in `X` such that `t` is preirreducible, `U` is open and nonempty, and `U` is a subset of `S` which in turn is a subset of `t`, then the set `S` is irreducible.
In the context of topology, a preirreducible set is one where there is no non-trivial pair of disjoint open sets, and an irreducible set is one that is nonempty and doesn't separate into two non-trivial open disjoint sets. This theorem essentially provides a condition under which a subset of a preirreducible set can be verified as irreducible.
More concisely: If `t` is a preirreducible, nonempty open set in a topological space `X`, and `S` is a nonempty subset of `t` that is contained in an open set `U` also contained in `t`, then `S` is irreducible.
|
isIrreducible_singleton
theorem isIrreducible_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, IsIrreducible {x}
The theorem `isIrreducible_singleton` states that for any type `X` equipped with a topological space structure and any element `x` of `X`, the singleton set containing just `x` is an irreducible set. In other words, this singleton set is non-empty and there is no pair of disjoint open sets within it, which are both non-empty when intersected with the singleton set.
More concisely: For any topological space `(X,τ)` and element `x ∈ X`, the singleton set `{x} ⊆ X` is an irreducible set, i.e., there do not exist disjoint non-empty open sets `U,V ∈ τ` such that `x ∈ U ∩ V`.
|
IsIrreducible.closure
theorem IsIrreducible.closure :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsIrreducible s → IsIrreducible (closure s)
This theorem states that if a set `s` is irreducible in a topological space `X`, then the closure of `s` is also irreducible in `X`. Here, a set is said to be irreducible if it is nonempty and there is no non-trivial pair of disjoint open subsets within it. The closure of a set `s` is defined as the smallest closed set that contains `s`.
More concisely: If a nonempty set `s` is irreducible in a topological space `X`, then the closure of `s` is also irreducible in `X`.
|
isIrreducible_iff_sUnion_closed
theorem isIrreducible_iff_sUnion_closed :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
IsIrreducible s ↔ ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed z) → s ⊆ (↑t).sUnion → ∃ z ∈ t, s ⊆ z
This theorem states that a set is irreducible if and only if for every cover of the set by a finite collection of closed sets, the set is contained in one of the members of the collection. More explicitly, for any type 'X' with a topology and any set 's' of type 'X', 's' is irreducible if and only if for any finite set 't' of sets of type 'X', if every set in 't' is closed and 's' is a subset of the union of all sets in 't', then there exists a set in 't' that contains 's'.
More concisely: A set is irreducible if and only if it is contained in at least one member of any finite collection of closed sets that covers it.
|
isIrreducible_iff_sInter
theorem isIrreducible_iff_sInter :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
IsIrreducible s ↔
∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ (↑U).sInter).Nonempty
The theorem `isIrreducible_iff_sInter` states that, for any type `X` equipped with a topological space structure and any set `s` of elements of type `X`, `s` is irreducible if and only if the following holds: For every finite collection `U` of open sets such that each member of `U` intersects `s`, it is also the case that `s` intersects the intersection of all members of `U`. In other words, there is an element of `s` that is contained in every member of the collection `U`.
More concisely: A set `s` in a topological space `X` is irreducible if and only if for every finite collection `U` of open sets intersecting `s`, their intersection also intersects `s`.
|
isPreirreducible_singleton
theorem isPreirreducible_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, IsPreirreducible {x} := by
sorry
The theorem `isPreirreducible_singleton` states that for any type `X` equipped with a topology (a topological space), every singleton set (a set containing exactly one element) `{x}` is a preirreducible set. In mathematical terms, this means if we take any two open sets `u` and `v` in `X` such that the intersection of `u` or `v` with the singleton `{x}` is nonempty, then the intersection of `u`, `v`, and `{x}` is also nonempty. This is to say, there are no non-trivial pair of disjoint open sets in the singleton `{x}`.
More concisely: For any topological space (X, top X) and any point x ∈ X, the singleton set {x} is a preirreducible open set, i.e., for all open sets U, V ∈ top X with x ∈ U ∩ V, we have U ∩ V ∩ {x} ≠ ∅.
|
isClosed_of_mem_irreducibleComponents
theorem isClosed_of_mem_irreducibleComponents :
∀ {X : Type u_1} [inst : TopologicalSpace X], ∀ s ∈ irreducibleComponents X, IsClosed s
This theorem states that for any given type `X` that has a topology associated with it (denoted by `[inst : TopologicalSpace X]`), all elements `s` in the set of irreducible components of `X` (`irreducibleComponents X`) are closed sets. In other words, if a subset `s` of a topological space `X` is an irreducible component of `X`, then `s` is a closed set in that topology.
More concisely: For any topological space `X` and each of its irreducible components `s`, `s` is a closed subset of `X`.
|
IsPreirreducible.closure
theorem IsPreirreducible.closure :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsPreirreducible s → IsPreirreducible (closure s) := by
sorry
This theorem is stating that for any type `X` that has a topological space structure and for any set `s` of this type, if `s` is preirreducible, then the closure of `s` is also preirreducible. In more mathematical terms, if a set `s` in a topological space `X` is such that for any pair of open subsets `u` and `v` of `X`, if their intersections with `s` are nonempty, then their intersection also intersects `s`, then the same property holds for the closure of `s` (the smallest closed set containing `s` in `X`). The theorem is a reverse direction version of another theorem named `isPreirreducible_iff_closure`.
More concisely: If `s` is a preirreducible subset of a topological space `X`, then the closure of `s` is also a preirreducible subset of `X`.
|
PreirreducibleSpace.isPreirreducible_univ
theorem PreirreducibleSpace.isPreirreducible_univ :
∀ {X : Type u_3} [inst : TopologicalSpace X] [self : PreirreducibleSpace X], IsPreirreducible Set.univ
This theorem states that in a preirreducible topological space, the universal set, which contains all elements of the space, is also preirreducible. In more detail, given any topological space that has the property of being preirreducible, if you consider any two open sets in this space, and if there is at least one element from the universal set in each of these open sets, then there is also at least one element from the universal set in the intersection of these two open sets.
More concisely: In a preirreducible topological space, the intersection of any two open sets containing elements from the universal set is non-empty.
|
IsOpen.dense
theorem IsOpen.dense :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [inst_1 : PreirreducibleSpace X],
IsOpen s → s.Nonempty → Dense s
This theorem states that in a (pre)irreducible topological space, any nonempty open set is dense. This means for any point in the topological space, it belongs to the closure of the given nonempty open set. In other words, given a topological space and a nonempty open set within it, every point in the space is either in the open set or is a limit point of the open set, if the space is (pre)irreducible.
More concisely: In a (pre)irreducible topological space, every nonempty open set is dense, i.e., the closure of any open set equals the topological space itself.
|
IrreducibleSpace.isIrreducible_univ
theorem IrreducibleSpace.isIrreducible_univ :
∀ (X : Type u_3) [inst : TopologicalSpace X] [inst_1 : IrreducibleSpace X], IsIrreducible Set.univ
The theorem `IrreducibleSpace.isIrreducible_univ` asserts that for any type `X` equipped with a topological space structure and such that the topological space is irreducible (as specified by `IrreducibleSpace X`), the universal set (which contains all elements of `X`) is irreducible. In other words, the universal set is nonempty and there is no pair of disjoint open sets in it that cover it completely apart from the trivial pair where one of the sets is the empty set.
More concisely: If `X` is an irreducible topological space, then its universal set is also an irreducible subset.
|
isPreirreducible_iff_closed_union_closed
theorem isPreirreducible_iff_closed_union_closed :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
IsPreirreducible s ↔ ∀ (z₁ z₂ : Set X), IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
The theorem `isPreirreducible_iff_closed_union_closed` states that for any type `X` endowed with a topological space structure, a set `s` of `X` is preirreducible if and only if for every cover of `s` by two closed sets `z₁` and `z₂`, `s` is contained in either `z₁` or `z₂`. In other words, it is impossible to cover a preirreducible set with two closed sets without the set being completely contained within one of the covering closed sets.
More concisely: A set in a topological space is preirreducible if and only if it cannot be covered by two closed sets without being contained in one of them.
|
IsIrreducible.nonempty
theorem IsIrreducible.nonempty :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsIrreducible s → s.Nonempty
The theorem `IsIrreducible.nonempty` states that for any type `X` equipped with a topological space structure, and any set `s` of type `X`, if the set `s` is irreducible, then `s` is nonempty. In other words, there cannot exist an irreducible set that is empty. This means an irreducible set, by definition, must contain at least one element.
More concisely: An irreducible subset of a topological space is nonempty.
|