English
Two distinct points have distinct Dirac measures.
Русский
Две разные точки соответствуют различным мерам Дирака.
LaTeX
$$$\\text{If } x \\neq y, \\; \\mathrm{dirac}_x \\neq \\mathrm{dirac}_y$$$
Lean4
theorem exists_BCNN {X : Type*} [TopologicalSpace X] [CompletelyRegularSpace X] {K : Set X} (K_closed : IsClosed K)
{x : X} (x_notin_K : x ∉ K) : ∃ (f : X →ᵇ ℝ≥0), f x = 1 ∧ (∀ y ∈ K, f y = 0) :=
by
obtain ⟨g, g_cont, gx_zero, g_one_on_K⟩ := CompletelyRegularSpace.completely_regular x K K_closed x_notin_K
have g_bdd : ∀ x y, dist (Real.toNNReal (g x)) (Real.toNNReal (g y)) ≤ 1 :=
by
refine fun x y ↦ ((Real.lipschitzWith_toNNReal).dist_le_mul (g x) (g y)).trans ?_
simpa using Real.dist_le_of_mem_Icc_01 (g x).prop (g y).prop
set g' :=
BoundedContinuousFunction.mkOfBound ⟨fun x ↦ Real.toNNReal (g x), continuous_real_toNNReal.comp g_cont.subtype_val⟩
1 g_bdd
set f := 1 - g'
refine ⟨f, by simp [f, g', gx_zero], fun y y_in_K ↦ by simp [f, g', g_one_on_K y_in_K, tsub_self]⟩
