English
There exists a continuous function with compact support whose values are nonnegative and nonzero at a given point.
Русский
Существует непрерывная функция с компактной поддержкой, значения которой неотрицательны и не равны нулю в некоторой точке.
LaTeX
$$$\exists f \in C(X, \mathbb{R}), HasCompactSupport f, 0 \le f, f(x) \neq 0$$$
Lean4
theorem exists_continuous_nonneg_pos [RegularSpace X] [LocallyCompactSpace X] (x : X) :
∃ f : C(X, ℝ), HasCompactSupport f ∧ 0 ≤ (f : X → ℝ) ∧ f x ≠ 0 :=
by
rcases exists_compact_mem_nhds x with ⟨k, hk, k_mem⟩
rcases exists_continuous_one_zero_of_isCompact hk isClosed_empty (disjoint_empty k) with ⟨f, fk, -, f_comp, hf⟩
refine ⟨f, f_comp, fun x ↦ (hf x).1, ?_⟩
have := fk (mem_of_mem_nhds k_mem)
simp only [Pi.one_apply] at this
simp [this]
