instInfOpenNormalSubgroup — Mathlib

English

The infimum (meet) of two open normal subgroups is their intersection; in particular, U ∩ V is open normal.

Русский

Наименьшее (пересечение) двух открытых нормальных подгрупп есть их пересечение; и U ∩ V является открытой нормальной подгруппой.

LaTeX

$$U ∧ V = U ∩ V; the intersection is open and normal.$$

Lean4

@[to_additive]
instance instInfOpenNormalSubgroup : Min (OpenNormalSubgroup G) :=
  ⟨fun U V ↦ ⟨U.toOpenSubgroup ⊓ V.toOpenSubgroup, Subgroup.normal_inf_normal U.toSubgroup V.toSubgroup⟩⟩

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