theorem smooth_urysohn_support_Ioo {a b c d : ℝ} (h1 : a < b) (h3 : c < d) : ∃ (Ψ : ℝ → ℝ), ContDiff ℝ (↑⊤) Ψ ∧ HasCompactSupport Ψ ∧ (Set.Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Set.Ioo a d).indicator 1 ∧ Function.support Ψ = Set.Ioo a d

theorem SmoothExistence : ∃ (ν : ℝ → ℝ), ContDiff ℝ (↑⊤) ν ∧ (∀ (x : ℝ), 0 ≤ ν x) ∧ Function.support ν ⊆ Set.Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Set.Ici 0, ν x / x = 1