English
Group topologies on γ form a complete lattice, with ⊥ the discrete topology and ⊤ the indiscrete topology; infimum is the topology generated by all open sets; the supremum is the infimum of all group topologies contained in the intersection.
Русский
Групповые топологии на γ образуют полную решётку: ⊥ — дискретная топология, ⊤ — недискретная; инфимуm порождается открытыми множествами; супремум — инфиму имени группы топологий, содержащихся в пересечении.
LaTeX
$$$\\text{CompleteSemilatticeInf}(\\mathrm{GroupTopology}(\\alpha))$$$
Lean4
/-- Group topologies on `γ` form a complete lattice, with `⊥` the discrete topology and `⊤` the
indiscrete topology.
The infimum of a collection of group topologies is the topology generated by all their open sets
(which is a group topology).
The supremum of two group topologies `s` and `t` is the infimum of the family of all group
topologies contained in the intersection of `s` and `t`. -/
@[to_additive /-- Group topologies on `γ` form a complete lattice, with `⊥` the discrete topology and
`⊤` the indiscrete topology.
The infimum of a collection of group topologies is the topology generated by all their open sets
(which is a group topology).
The supremum of two group topologies `s` and `t` is the infimum of the family of all group
topologies contained in the intersection of `s` and `t`. -/
]
instance : CompleteSemilatticeInf (GroupTopology α) :=
{ inferInstanceAs (InfSet (GroupTopology α)),
inferInstanceAs
(PartialOrder
(GroupTopology
α)) with
sInf_le := fun _ a haS => toTopologicalSpace_le.1 <| sInf_le ⟨a, haS, rfl⟩
le_sInf := by
intro S a hab
apply (inferInstanceAs (CompleteLattice (TopologicalSpace α))).le_sInf
rintro _ ⟨b, hbS, rfl⟩
exact hab b hbS }
