English
Let α be a fixed group. The collection of all group topologies on α forms a complete lattice under the refinement order: the meet of two topologies is their intersection, the top element is the discrete topology, and the bottom element is the indiscrete topology.
Русский
Пусть α — фиксированная группа. Набор всех групповых топологий на α образует полную решётку относительно порядка refinement: встреча двух топологий есть их пересечение, верхний элемент — дискретная топология, нижний элемент — indiscrete (незаданная) топология.
LaTeX
$$$\\text{Let } \\mathcal G(\\alpha) = \\{ \\tau : \\text{topology on } \\alpha \\text{ making } \\alpha \\text{ a topological group} \\}. \\\\ (\\mathcal G(\\alpha), \\le) \\\\ \\text{is a complete lattice with } \\tau_1 \\wedge \\tau_2 = \\tau_1 \\cap \\tau_2, \\quad \\top = \\text{DiscreteTop}(\\alpha), \\quad \\bot = \\text{IndiscreteTop}(\\alpha).$$$
Lean4
@[to_additive]
instance : CompleteLattice (GroupTopology α) :=
{ inferInstanceAs (BoundedOrder (GroupTopology α)), inferInstanceAs (SemilatticeInf (GroupTopology α)),
completeLatticeOfCompleteSemilatticeInf _ with
inf := (· ⊓ ·)
top := ⊤
bot := ⊥ }
