English
A group acts properly on X if and only if the action is continuous and a certain ultrafilter convergence property holds: for every ultrafilter on G×X, if the pushforward along (g,x) ↦ (g•x, x) converges to (x1, x2), then there is g with g•x2 = x1 and Tendsto Prod.fst along the ultrafilter converging to g.
Русский
Группа действует корректно на X тогда и только тогда, когда действие непрерывно и выполняется требование предельности по ультрафильтрам: для любого ультрафильтра на G×X, если образ по (g,x) → (g•x, x) сходится к (x1, x2), то существует g с g•x2 = x1 и Tendsto Prod.fst по ультрафильтру сходится к g.
LaTeX
$$$\\text{ProperSMul } G X \\;\\Leftrightarrow\\; \\Big(\\text{ContinuousSMul } G X \\land\\; \\forall 𝒰:\\, Ultrafilter (G \\times X),\\ \\forall x_1,x_2:\\, X,\\; \\mathrm{Tendsto}(\\mathrm{fun }g x \\mapsto (g\\cdot x, x))\\, 𝒰\\, (\\mathcal N (x_1,x_2)) \\Rightarrow \\exists g:\\, G,\\ x_1=g\\cdot x_2 \\land \\mathrm{Tendsto}(\\mathrm{Prod.fst})\\; 𝒰\\; (\\mathcal N g) \\Big)$$$
Lean4
/-- A group `G` acts properly on a T2 topological space `X` if and only if for all ultrafilters
`𝒰` on `X × G`, if `𝒰` converges to `(x₁, x₂)` along the map `(g, x) ↦ (g • x, x)`,
then there exists `g : G` such that `𝒰.fst` converges to `g`. -/
theorem properSMul_iff_continuousSMul_ultrafilter_tendsto_t2 [T2Space X] :
ProperSMul G X ↔
ContinuousSMul G X ∧
(∀ 𝒰 : Ultrafilter (G × X),
∀ x₁ x₂ : X,
Tendsto (fun gx : G × X ↦ (gx.1 • gx.2, gx.2)) 𝒰 (𝓝 (x₁, x₂)) →
∃ g : G, Tendsto (Prod.fst : G × X → G) 𝒰 (𝓝 g)) :=
by
rw [properSMul_iff_continuousSMul_ultrafilter_tendsto]
refine and_congr_right fun hc ↦ ?_
congrm ∀ 𝒰 x₁ x₂ hxx, ∃ g, ?_
exact
and_iff_right_of_imp fun hg ↦
tendsto_nhds_unique (hg.smul ((continuous_snd.tendsto _).comp hxx)) ((continuous_fst.tendsto _).comp hxx)
