Urysohns.CU.approx_le_one
theorem Urysohns.CU.approx_le_one :
∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Prop} (c : Urysohns.CU P) (n : ℕ) (x : X),
Urysohns.CU.approx n c x ≤ 1
This theorem states that for any type 'X' equipped with a topological space structure, any predicate 'P' on the set of 'X', any Urysohn's lemma function 'c' based on 'P', any natural number 'n', and any element 'x' of type 'X', the Urysohn's lemma approximation function `Urysohns.CU.approx` applied to 'n', 'c', and 'x' will always be less than or equal to one. In other words, it guarantees that the values generated by Urysohn's lemma approximation function will not exceed one.
More concisely: For any topological space 'X' and predicate 'P' on 'X', the Urysohn's lemma approximation function `Urysohns.CU.approx` applied to any Urysohn's lemma function 'c' based on 'P', any natural number 'n', and any element 'x' in 'X' satisfies `Urysohns.CU.approx n c x ≤ 1`.
|
exists_continuous_one_zero_of_isCompact
theorem exists_continuous_one_zero_of_isCompact :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : RegularSpace X] [inst_2 : LocallyCompactSpace X]
{s t : Set X},
IsCompact s →
IsClosed t →
Disjoint s t →
∃ f, Set.EqOn (⇑f) 1 s ∧ Set.EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
Urysohn's Lemma: In the context of a regular locally compact topological space `X`, given two disjoint sets `s` and `t` where `s` is compact and `t` is closed, there exists a function `f : X → ℝ` that is continuous, has compact support and satisfies the following properties:
- The function `f` is equal to 1 on the set `s`.
- The function `f` is equal to 0 on the set `t`.
- For all `x` in `X`, the function `f` takes a value between 0 and 1 inclusive, i.e., `0 ≤ f(x) ≤ 1`.
More concisely: In a regular locally compact topological space, given disjoint compact and closed sets, there exists a continuous real-valued function with compact support that takes the value 1 on one set and 0 on the other, and everywhere in between.
|
Urysohns.CU.continuous_lim
theorem Urysohns.CU.continuous_lim :
∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Prop} (c : Urysohns.CU P), Continuous c.lim
This theorem states the continuity of the limit function of Urysohn's C(U) construction. Given any type `X` which has a topological space structure, and any `P` which is a predicate on sets of `X`, for any Urysohn's C(U) construction `c` based on `P`, the limit function `c.lim` is continuous. This theorem is part of the proof strategies for Urysohn's lemma in topology.
More concisely: The limit function of a Urysohn's C(U) construction based on a predicate P, defined on a topological space X, is continuous.
|
exists_continuous_zero_one_of_isClosed
theorem exists_continuous_zero_one_of_isClosed :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : NormalSpace X] {s t : Set X},
IsClosed s →
IsClosed t → Disjoint s t → ∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
Urysohn's Lemma states that given a normal topological space `X` and two disjoint closed sets `s` and `t` within that space, there exists a continuous function `f` from `X` to the real numbers with the following properties:
- `f` equals zero for all points in set `s`;
- `f` equals one for all points in set `t`;
- For all points `x` in the topological space `X`, the value of `f(x)` lies in the closed interval from 0 to 1, inclusive.
In other words, we can always find a function that smoothly transitions from 0 to 1 across the space, separating the two sets.
More concisely: Given a normal topological space and two disjoint closed sets, there exists a continuous function mapping every point in the first set to 0, every point in the second set to 1, and with values in between for all other points.
|
exists_continuous_zero_one_of_isCompact
theorem exists_continuous_zero_one_of_isCompact :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : RegularSpace X] [inst_2 : LocallyCompactSpace X]
{s t : Set X},
IsCompact s →
IsClosed t → Disjoint s t → ∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
Urysohn's Lemma states that, given two disjoint sets `s` and `t` in a regular and locally compact topological space `X`, with `s` being a compact set and `t` being a closed set, there exists a continuous function `f` mapping from `X` to the real numbers such that the function `f` equals zero for all elements in `s`, equals one for all elements in `t`, and the output of `f` for any element in `X` lies within the closed interval from 0 to 1, inclusive. This theorem provides a means of interpolating between two separate points (sets in this case) in a continuous manner in a topological context.
More concisely: Given a regular and locally compact topological space X, any pair of disjoint compact (s) and closed (t) sets admit a continuous function f: X → ℝ with 0 ≤ f ≤ 1 such that f(s) = {0} and f(t) = {1}.
|
exists_continuous_one_zero_of_isCompact_of_isGδ
theorem exists_continuous_one_zero_of_isCompact_of_isGδ :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : RegularSpace X] [inst_2 : LocallyCompactSpace X]
{s t : Set X},
IsCompact s →
IsGδ s →
IsClosed t →
Disjoint s t →
∃ f, s = ⇑f ⁻¹' {1} ∧ Set.EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
Urysohn's Lemma asserts that given a regular locally compact topological space `X`, if `s` and `t` are two disjoint sets within `X` where `s` is compact and `t` is closed, then there exists a continuous function `f : X → ℝ` that has compact support and satisfies the following conditions:
1. `f` equals one on the set `s`,
2. `f` equals zero on the set `t`,
3. `f(x)` ranges between 0 and 1 for every `x` in `X`.
Furthermore, if `s` is a Gδ set (a countable intersection of open sets), then the inverse image of `1` under `f` is precisely the set `s`.
More concisely: Given a regular locally compact space `X`, if `s` is a compact, disjoint, and Gδ subset of a closed set `t` in `X`, then there exists a continuous function `f : X → ℝ` with compact support that equals one on `s` and equals zero on `t`, with values between 0 and 1 on all of `X`.
|