English
If 1 ∈ s and 1 ∈ t for sets s ⊆ M, t ⊆ N, then the closure of s × t equals the product of closures: closure(s × t) = closure(s) .prod closure(t).
Русский
Пусть 1 ∈ s и 1 ∈ t, тогда замыкание множества s × t равно произведению замыканий: closure(s × t) = closure(s) .prod closure(t).
LaTeX
$$$$ \\operatorname{closure}(s \\times t) = \\operatorname{closure}(s) \\;\\mathrm{prod}\\; \\operatorname{closure}(t) $$$$
Lean4
@[to_additive closure_prod]
theorem closure_prod {s : Set M} {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_of_le_comap _ <| closure_le.2 fun _x hx => subset_closure ⟨hx, ht⟩,
map_le_of_le_comap _ <| closure_le.2 fun _y hy => subset_closure ⟨hs, hy⟩⟩)
