instMaxOfContinuousMul — Mathlib

English

There is a maximum operation on OpenNormalSubgroup G coming from the maximum of their open subgroups, yielding an OpenNormalSubgroup.

Русский

Существует операция максимума на OpenNormalSubgroup G, получаемая как максимум их открытых подпгрупп, дающая открытую нормальную подгруппу.

LaTeX

$$Max(OpenNormalSubgroup G)$$

Lean4

@[to_additive]
instance [ContinuousMul G] : Max (OpenNormalSubgroup G) :=
  ⟨fun U V ↦ ⟨U.toOpenSubgroup ⊔ V.toOpenSubgroup, Subgroup.sup_normal U.toOpenSubgroup.1 V.toOpenSubgroup.1⟩⟩

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