English
Let s and t be disjoint closed subsets of a Hausdorff, σ-compact, finite-dimensional manifold M. Then there exists a smooth function f: M → ℝ whose values lie in [0,1], such that f vanishes exactly on s and equals 1 exactly on t.
Русский
Пусть s и t — непересекающиеся замкнутые подмножества гамного многообразия M, удовлетворяющего условию Хаусдорфа, σ-сжатости и конечной размерности. Тогда существует гладкая функция f: M → ℝ, значения которой лежат в [0,1], такая что f(x)=0 ⇔ x∈s и f(x)=1 ⇔ x∈t.
LaTeX
$$$$\\exists f: M \\to \\mathbb{R},\\quad f \\text{ гладкая},\\quad \\operatorname{range}(f) \\subseteq [0,1],\\quad (\\forall x\\in M)(x\\in s \\iff f(x)=0),\\quad (\\forall x\\in M)(x\\in t \\iff f(x)=1).$$$$
Lean4
/-- Given two disjoint closed sets `s, t` in a Hausdorff σ-compact finite-dimensional manifold,
there exists an infinitely smooth function that is equal to `0` exactly on `s` and to `1`
exactly on `t`. See also `exists_smooth_zero_one_of_isClosed` for a slightly weaker version. -/
theorem exists_msmooth_zero_iff_one_iff_of_isClosed {s t : Set M} (hs : IsClosed s) (ht : IsClosed t)
(hd : Disjoint s t) :
∃ f : M → ℝ, ContMDiff I 𝓘(ℝ) ∞ f ∧ range f ⊆ Icc 0 1 ∧ (∀ x, x ∈ s ↔ f x = 0) ∧ (∀ x, x ∈ t ↔ f x = 1) :=
by
rcases exists_msmooth_support_eq_eq_one_iff I hs.isOpen_compl ht hd.subset_compl_left with
⟨f, f_diff, f_range, fs, ft⟩
refine ⟨f, f_diff, f_range, ?_, ft⟩
simp [← notMem_support, fs]
