instance metrizable_of_lcsc (X : Type u_1) [TopologicalSpace X] [SecondCountableTopology X] [LocallyCompactSpace X] [T2Space X] : TopologicalSpace.MetrizableSpace X

noncomputable def ContinuousMap.liftReal {X : Type u_1} [MetricSpace X] (f : C(X, ℝ)) : C(X, ℂ)

noncomputable def diracCLM {X : Type u_1} [MetricSpace X] (x : X) : WeakDual ℂ C(X, ℂ)

noncomputable def diracPOUApprox {X : Type u_1} [MetricSpace X] (μ : WeakDual ℂ C(X, ℂ)) (S : Finset X) (φ : ↥S → C(X, ℝ)) : WeakDual ℂ C(X, ℂ)

theorem diracPOUApprox_eval_sub_tendsto {X : Type u_1} [MetricSpace X] [CompactSpace X] (μ : WeakDual ℂ C(X, ℂ)) (S : ℕ → Finset X) (φ : (n : ℕ) → PartitionOfUnity (↥(S n)) X) (ε_seq : ℕ → ℝ) (hε_pos : ∀ (n : ℕ), 0 < ε_seq n) (hε_lim : Filter.Tendsto ε_seq Filter.atTop (nhds 0)) (hsubord : ∀ (n : ℕ), (φ n).IsSubordinate fun (s : ↥(S n)) => Metric.ball (↑s) (ε_seq n)) (f : C(X, ℂ)) : Filter.Tendsto (fun (n : ℕ) => (diracPOUApprox μ (S n) ((φ n).toFun Set.univ)) f) Filter.atTop (nhds (μ f))