instSemilatticeInfOpenNormalSubgroup

English

The infimum of open normal subgroups U and V is their intersection, realized as an open normal subgroup.

Русский

Пусть U и V — открытые нормальные подгруппы; их инфимум равен их пересечению, которое сама является открытой нормальной подгруппой.

LaTeX

$$min(U,V) = U ∩ V$$

Lean4

@[to_additive]
instance instSemilatticeInfOpenNormalSubgroup : SemilatticeInf (OpenNormalSubgroup G) :=
  SetLike.coe_injective.semilatticeInf ((↑) : OpenNormalSubgroup G → Set G) fun _ _ ↦ rfl

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