exists_smooth_one_nhds_of_subset_interior

English

There exists a smooth function f: M→[0,1] separating closed sets s,t with f=0 near s and f=1 near t.

Русский

Существует гладкая функция f: M→[0,1], которая равна 0 в окрестности s и 1 в окрестности t.

LaTeX

$$$\\exists f: C^\\infty(I,M; 𝓘(ℝ),ℝ), f|_s=0, f|_t=1, 0≤f≤1$$$

Lean4

/-- Given two sets `s, t` in a Hausdorff normal σ-compact finite-dimensional manifold `M`
with `s` open and `s ⊆ interior t`, there is a smooth function `f : M → [0,1]` which is equal to `s`
in a neighbourhood of `s` and has support contained in `t`. -/
theorem exists_smooth_one_nhds_of_subset_interior [T2Space M] [NormalSpace M] [SigmaCompactSpace M] {s t : Set M}
    (hs : IsClosed s) (hd : s ⊆ interior t) :
    ∃ f : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, (∀ᶠ x in 𝓝ˢ s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ ∀ x, f x ∈ Icc 0 1 :=
  by
  rcases
    exists_smooth_zero_one_nhds_of_isClosed I isOpen_interior.isClosed_compl hs
      (by rwa [← subset_compl_iff_disjoint_left, compl_compl]) with
    ⟨f, h0, h1, hf⟩
  refine ⟨f, h1, fun x hx ↦ ?_, hf⟩
  exact h0.self_of_nhdsSet _ fun hx' ↦ hx <| interior_subset hx'

Похожие утверждения