English
If G acts properly on X, the quotient space by the orbit relation is Hausdorff (T2).
Русский
Если G действует корректно на X, то фактор-пространство по орбитальной Relation является Гаусдорфовым (T2).
LaTeX
$$$T2Space\\big(\\text{Quotient}(\\text{MulAction.orbitRel } G X)\\big)$$$
Lean4
/-- If `G` acts properly on `X`, then the quotient space is Hausdorff (T2). -/
@[to_additive /-- If `G` acts properly on `X`, then the quotient space is Hausdorff (T2). -/
]
theorem t2Space_quotient_mulAction_of_properSMul [ProperSMul G X] : T2Space (Quotient (MulAction.orbitRel G X)) :=
by
rw [t2_iff_isClosed_diagonal]
set R := MulAction.orbitRel G X
let π : X → Quotient R := Quotient.mk'
have : IsOpenQuotientMap (Prod.map π π) :=
MulAction.isOpenQuotientMap_quotientMk.prodMap MulAction.isOpenQuotientMap_quotientMk
rw [← this.isQuotientMap.isClosed_preimage]
convert ProperSMul.isProperMap_smul_pair.isClosedMap.isClosed_range
· ext ⟨x₁, x₂⟩
simp only [mem_preimage, map_apply, mem_diagonal_iff, mem_range, Prod.mk.injEq, Prod.exists, exists_eq_right]
rw [Quotient.eq', MulAction.orbitRel_apply, MulAction.mem_orbit_iff]
all_goals infer_instance
