instLatticeOfContinuousMul — Mathlib

English

There is a lattice structure on OpenNormalSubgroup G with the standard meet and join operations, inherited from the ambient lattice on subgroups.

Русский

Для OpenNormalSubgroup G существует решетка с обычными операциями meet и join, наследованными от окружающей решетки подгрупп.

LaTeX

$$instLatticeOfContinuousMul: Lattice(OpenNormalSubgroup G)$$

Lean4

@[to_additive]
instance [ContinuousMul G] : Lattice (OpenNormalSubgroup G) :=
  { instSemilatticeInfOpenNormalSubgroup, instSemilatticeSupOpenNormalSubgroup with
    toPartialOrder := instPartialOrderOpenNormalSubgroup }

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