English
supClosure distributes over product: supClosure(s × t) = supClosure s × supClosure t.
Русский
supClosure сохраняет произведение: supClosure(s × t) = supClosure s × supClosure t.
LaTeX
$$$\\operatorname{supClosure}(s \\times t) = \\operatorname{supClosure}(s) \\times \\operatorname{supClosure}(t)$$$
Lean4
@[simp]
theorem supClosure_prod (s : Set α) (t : Set β) : supClosure (s ×ˢ t) = supClosure s ×ˢ supClosure t :=
le_antisymm
(supClosure_min (Set.prod_mono subset_supClosure subset_supClosure) <|
supClosed_supClosure.prod supClosed_supClosure) <|
by
rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩
refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
· simpa only [coe_product] using Set.prod_mono hus hvt
· simp [prodMk_sup'_sup']
