Perfect.small_diam_splitting
theorem Perfect.small_diam_splitting :
∀ {α : Type u_1} [inst : MetricSpace α] {C : Set α},
Perfect C →
∀ {ε : ENNReal},
C.Nonempty →
0 < ε →
∃ C₀ C₁,
(Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
(Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁
The theorem `Perfect.small_diam_splitting` is a refinement of a splitting operation for metric spaces, specifically for perfect sets which are subsets of the metric space. In the context of this theorem, a set is said to be perfect if it is closed and has no isolated points. Given a perfect set `C` in a metric space and a positive extended nonnegative real number `ε`, the theorem states that there exists two perfect sets `C₀` and `C₁` such that:
- Both `C₀` and `C₁` are nonempty subsets of `C`.
- The diameter of both `C₀` and `C₁` (defined as the supremum of the distances between all pairs of points in the set) is less than or equal to `ε`.
- The sets `C₀` and `C₁` are disjoint, defined in this context as their infimum being the bottom element of the order. This implies that there is no element common to both `C₀` and `C₁`.
In other words, the theorem guarantees the ability to split a given perfect set into two disjoint perfect sets of smaller diameter.
More concisely: Given a perfect set in a metric space and a positive extended real number, there exist disjoint perfect subsets with diameter less than or equal to the given number.
|
IsClosed.exists_nat_bool_injection_of_not_countable
theorem IsClosed.exists_nat_bool_injection_of_not_countable :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : PolishSpace α] {C : Set α},
IsClosed C → ¬C.Countable → ∃ f, Set.range f ⊆ C ∧ Continuous f ∧ Function.Injective f
This theorem states that for any closed, uncountable subset of a Polish space, there exists a continuous injection from the Cantor space, which is the set of all sequences of boolean values indexed by natural numbers. In other words, if we have a Polish space (a completely separable and metrizable topological space), and if there is a closed subset within this space that is not countable, then there is a function that can continuously and injectively map every sequence of boolean values (true or false) indexed by natural numbers to this subset. This function is such that every point in the image of the function is in the subset and there are no repetitions in the mapped values.
More concisely: Given a Polish space with a closed, uncountable subset, there exists a continuous injection from the Cantor space to that subset.
|
Perfect.exists_nat_bool_injection
theorem Perfect.exists_nat_bool_injection :
∀ {α : Type u_1} [inst : MetricSpace α] {C : Set α},
Perfect C →
C.Nonempty → ∀ [inst_1 : CompleteSpace α], ∃ f, Set.range f ⊆ C ∧ Continuous f ∧ Function.Injective f
This theorem states that for any nonempty perfect set in a complete metric space, there exists a continuous injection from the Cantor space (the space of all sequences of boolean values indexed by natural numbers). In other words, given a type `α` that forms a metric space and a perfect set `C` of this type that is nonempty, in the context where `α` also forms a complete space, the theorem asserts the existence of a function `f` whose range is a subset of `C`, and this function `f` is both continuous and injective.
More concisely: Given a complete metric space `α` with a nonempty perfect subset `C`, there exists a continuous injection from the Cantor space to `C`.
|