exists_bounded_mem_Icc_of_closed_of_le
theorem exists_bounded_mem_Icc_of_closed_of_le :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : NormalSpace X] {s t : Set X},
IsClosed s →
IsClosed t →
Disjoint s t →
∀ {a b : ℝ},
a ≤ b →
∃ f,
Set.EqOn (⇑f) (Function.const X a) s ∧
Set.EqOn (⇑f) (Function.const X b) t ∧ ∀ (x : X), f x ∈ Set.Icc a b
Urysohn's lemma states that, given two disjoint closed sets `s` and `t` in a normal topological space `X`, and two real numbers `a` and `b` with `a` less than or equal to `b`, there exists a continuous function `f` from `X` to the set of real numbers such that `f` equals `a` on `s`, `f` equals `b` on `t`, and for all `x` in `X`, the value of `f(x)` lies in the closed interval from `a` to `b`. This theorem is a central result in topology, providing a way to separate disjoint closed sets with continuous functions.
More concisely: Given two disjoint closed sets in a normal topological space and two real numbers with one smaller than the other, there exists a continuous function mapping all sets elements to the interval between the two real numbers, equal to the first number on one set and the second number on the other.
|
exists_bounded_zero_one_of_closed
theorem exists_bounded_zero_one_of_closed :
∀ {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:** In a normal topological space `X`, if `s` and `t` are two disjoint closed sets, there exists a continuous function `f : X → ℝ` that satisfies the following conditions:
* The function `f` takes the value zero on each point of the set `s` and the value one on each point of the set `t`.
* For every element `x` in the topological space `X`, the value of the function `f` at `x` lies in the closed interval `[0, 1]`. This means the function `f` is bounded and its values are always between 0 and 1, inclusive.
More concisely: In a normal topological space, for every pair of disjoint closed sets, there exists a continuous function mapping all its points to the real numbers between 0 and 1, with values 0 on the first set and 1 on the second set.
|