English
If s ⊆ G and t ⊆ N contain the identity and closure, then closure(s × t) equals closure(s) × closure(t).
Русский
Если s ⊆ G и t ⊆ N содержат единицу и замкнуты, то замыкание s × t равно замыканию s × замыканию t.
LaTeX
$$$ \operatorname{closure}(s \times^{\mathrm{Set}} t) = \operatorname{closure}(s) \mathrm{prod} \operatorname{closure}(t) $$$
Lean4
@[to_additive closure_prod]
theorem closure_prod {s : Set G} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) :
closure (s ×ˢ t) = (closure s).prod (closure t) :=
le_antisymm (closure_le _ |>.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, subset_closure⟩)
(prod_le_iff.2
⟨map_le_iff_le_comap.2 <| closure_le _ |>.2 fun _x hx => subset_closure ⟨hx, ht⟩,
map_le_iff_le_comap.2 <| closure_le _ |>.2 fun _y hy => subset_closure ⟨hs, hy⟩⟩)
