instSemilatticeSupOpenNormalSubgroup

English

There is a SemilatticeSup structure on OpenNormalSubgroup G, compatible with the underlying Subgroup inclusions.

Русский

У OpenNormalSubgroup G есть структура SemilatticeSup, совместимая с вложением в подпгруппы.

LaTeX

$$instSemilatticeSupOpenNormalSubgroup: SemilatticeSup(OpenNormalSubgroup G)$$

Lean4

@[to_additive]
instance instSemilatticeSupOpenNormalSubgroup [ContinuousMul G] : SemilatticeSup (OpenNormalSubgroup G) :=
  toSubgroup_injective.semilatticeSup _ (fun _ _ ↦ rfl)

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