instPartialOrder — Mathlib

English

The group topologies on γ are partially ordered by refinement: t ≤ s if every open set in s is open in t.

Русский

Групповые топологии на γ образуют частично упорядоченное множество по включению (упрощению): t ≤ s тогда, когда любое открытое множество в s также открыто в t.

LaTeX

$$$\\text{PartialOrder}(\\mathrm{GroupTopology}(\\alpha))$$$

Lean4

/-- The ordering on group topologies on the group `γ`. `t ≤ s` if every set open in `s` is also open
in `t` (`t` is finer than `s`). -/
@[to_additive /-- The ordering on group topologies on the group `γ`. `t ≤ s` if every set open in `s`
      is also open in `t` (`t` is finer than `s`). -/
    ]
instance : PartialOrder (GroupTopology α) :=
  PartialOrder.lift toTopologicalSpace toTopologicalSpace_injective

Похожие утверждения