English
If a T1 group G acts properly on a space X, then X is Hausdorff (T2).
Русский
Если группа G с T1 свойством действует корректно на X, то X является Гаусдорфовым (T2).
LaTeX
$$$[T1Space G] \\Rightarrow (\\text{ProperSMul } G X) \\Rightarrow T2Space X$$$
Lean4
/-- If a T1 group acts properly on a topological space, then this topological space is T2. -/
@[to_additive /-- If a T1 group acts properly on a topological space,
then this topological space is T2. -/
]
theorem t2Space_of_properSMul_of_t1Group [h_proper : ProperSMul G X] [T1Space G] : T2Space X :=
by
let f := fun x : X ↦ ((1 : G), x)
have proper_f : IsProperMap f := by
refine IsClosedEmbedding.isProperMap ⟨?_, ?_⟩
· let g := fun gx : G × X ↦ gx.2
have : Function.LeftInverse g f := fun x ↦ by simp [f, g]
exact this.isEmbedding (by fun_prop) (by fun_prop)
· have : range f = ({ 1 } ×ˢ univ) := by simp [f, Set.singleton_prod]
rw [this]
exact isClosed_singleton.prod isClosed_univ
rw [t2_iff_isClosed_diagonal]
let g := fun gx : G × X ↦ (gx.1 • gx.2, gx.2)
have proper_g : IsProperMap g := (properSMul_iff G X).1 h_proper
have : g ∘ f = fun x ↦ (x, x) := by ext x <;> simp [f, g]
have range_gf : range (g ∘ f) = diagonal X := by simp [this]
rw [← range_gf]
exact (proper_g.comp proper_f).isClosed_range
