prod — Mathlib

English

The product of two open subgroups is an open subgroup of the product group.

Русский

Произведение двух открытых подгрупп является открытой подгруппой произведения групп.

LaTeX

$$$\forall U \in \mathrm{OpenSubgroup}(G),\forall V \in \mathrm{OpenSubgroup}(H):\ \mathrm{OpenSubgroup.prod}(U,V) \in \mathrm{OpenSubgroup}(G \times H)$$$

Lean4

/-- The product of two open subgroups as an open subgroup of the product group. -/
@[to_additive prod /-- The product of two open subgroups as an open subgroup of the product group. -/
    ]
def prod (U : OpenSubgroup G) (V : OpenSubgroup H) : OpenSubgroup (G × H) :=
  ⟨.prod U V, U.isOpen.prod V.isOpen⟩

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