English
A general tendsto result relating diracProbaEquiv.symm and filters in the range to Tendsto of identity.
Русский
Обобщённая формула предела для симметричной части эквив diracProba.
LaTeX
$$$\\text{Tendsto}(\\mathrm{diracProbaEquiv}^{-1}, F, \\mathcal{N}(\\mathrm{diracProbaEquiv}^{-1}\\mu)) \\iff \\text{Tendsto}(id, F, \\mathcal{N}(\\mu))$$$
Lean4
theorem tendsto_diracProbaEquivSymm_iff_tendsto [T0Space X] [CompletelyRegularSpace X] {μ : range (diracProba (X := X))}
(F : Filter (range (diracProba (X := X)))) :
Tendsto diracProbaEquiv.symm F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ) :=
by
have key := tendsto_diracProba_iff_tendsto (F.map diracProbaEquiv.symm) (x := diracProbaEquiv.symm μ)
rw [← (diracProbaEquiv (X := X)).symm_comp_self, ← tendsto_map'_iff] at key
simp only [tendsto_map'_iff, map_map, Equiv.self_comp_symm, map_id] at key
simp only [← key, diracProba_comp_diracProbaEquiv_symm_eq_val]
convert tendsto_subtype_rng.symm
exact apply_rangeSplitting (fun x ↦ diracProba x) μ
