English
Urysohns lemma: given disjoint closed sets, there exists a continuous function f with f = 0 on s, f = 1 on t, and 0 ≤ f ≤ 1 everywhere.
Русский
Лемма Урьсёна: при заданных непересекающихся замкнутых множествах существует непрерывная функция f, равная 0 на s, 1 на t и удовлетворяющая 0 ≤ f ≤ 1 на всей области.
LaTeX
$$$\exists f \in C(X, \mathbb{R}), f|_s = 0, f|_t = 1, \forall x\, f(x) \in Icc(0,1)$$$
Lean4
/-- Urysohn's lemma: if `s` and `t` are two disjoint closed sets in a normal topological space `X`,
then there exists a continuous function `f : X → ℝ` such that
* `f` equals zero on `s`;
* `f` equals one on `t`;
* `0 ≤ f x ≤ 1` for all `x`.
-/
theorem exists_continuous_zero_one_of_isClosed [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t)
(hd : Disjoint s t) : ∃ f : C(X, ℝ), EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
-- The actual proof is in the code above. Here we just repack it into the expected format.
let P : Set X → Set X → Prop := fun _ _ ↦ True
set c : Urysohns.CU P :=
{ C := s
U := tᶜ
P_C_U := trivial
closed_C := hs
open_U := ht.isOpen_compl
subset := disjoint_left.1 hd
hP := by
rintro c u c_closed - u_open cu
rcases normal_exists_closure_subset c_closed u_open cu with ⟨v, v_open, cv, hv⟩
exact ⟨v, v_open, cv, hv, trivial, trivial⟩ }
exact ⟨⟨c.lim, c.continuous_lim⟩, c.lim_of_mem_C, fun x hx => c.lim_of_notMem_U _ fun h => h hx, c.lim_mem_Icc⟩
