English
The existence of a complete lattice structure on the collection of group topologies is established; equalities of lattice components are encoded by the standard lattice axioms, guaranteeing infimum and top/bottom elements behave as expected.
Русский
Доказывается существование полной решетки над множеством групповых топологий, где инфимуум и верхний/нижний элементы ведут себя согласно стандартным аксиомам решетки.
LaTeX
$$$\\text{CompleteLattice}(\\text{GroupTopology}(\\alpha))\\quad\\text{with }\\inf,\\top,\\bot\\text{ as defined.}$$$
Lean4
@[to_additive]
theorem isClosedMap_quotient [CompactSpace α] :
letI := orbitRel α β
IsClosedMap (Quotient.mk' : β → Quotient (orbitRel α β)) :=
by
intro t ht
rw [← isQuotientMap_quotient_mk'.isClosed_preimage, MulAction.quotient_preimage_image_eq_union_mul]
convert ht.smul_left_of_isCompact (isCompact_univ (X := α))
rw [← biUnion_univ, ← iUnion_smul_left_image]
simp only [image_smul]
