English
Let U be an open subgroup of G and V an open subgroup of H. Then the product of U and V, viewed as a subset of G × H, is exactly the Cartesian product of their underlying sets: (U.prod V : Set (G × H)) = (U : Set G) × (V : Set H).
Русский
Пусть U — открытая подгруппа G, а V — открытая подгруппа H. Тогда произведение U и V, рассматриваемое как подмножество G × H, совпадает с декартовым произведением их множеств: (U.prod V : Set (G × H)) = (U : Set G) × (V : Set H).
LaTeX
$$$$(U \\mathrm{prod} V : \\mathrm{Set}(G \\times H)) = (U : \\mathrm{Set}G) \\times (V : \\mathrm{Set}H).$$$$
Lean4
@[to_additive (attr := simp, norm_cast) coe_prod]
theorem coe_prod (U : OpenSubgroup G) (V : OpenSubgroup H) : (U.prod V : Set (G × H)) = (U : Set G) ×ˢ (V : Set H) :=
rfl
