English
The inverse of the diracProbaEquiv is continuous (under T0 and completely regular assumptions).
Русский
Обратное отображение diracProbaEquiv непрерывно при условиях T0 и полного регуляра пространства.
LaTeX
$$$\\text{Continuous}(\\mathrm{diracProbaEquiv}^{-1})$$$
Lean4
/-- The assignment `x ↦ diracProba x` is continuous `X → ProbabilityMeasure X`. -/
theorem continuous_diracProba : Continuous (fun (x : X) ↦ diracProba x) :=
by
rw [continuous_iff_continuousAt]
apply fun x ↦ ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto.mpr fun f ↦ ?_
have f_mble : Measurable (fun X ↦ (f X : ℝ≥0∞)) := measurable_coe_nnreal_ennreal_iff.mpr f.continuous.measurable
simp only [diracProba, ProbabilityMeasure.coe_mk, lintegral_dirac' _ f_mble]
exact (ENNReal.continuous_coe.comp f.continuous).continuousAt
