English
For s,t ⊆ ℝ, the frontier of the complex prod is the union of two pieces: frontier(s ×ℂ t) = closure(s) ×ℂ frontier(t) ∪ frontier(s) ×ℂ closure(t).
Русский
Для множеств s,t ⊆ ℝ граница произведения в комплексной плоскости равна объединению двух частей: frontier(s ×ℂ t) = closure(s) ×ℂ frontier(t) ∪ frontier(s) ×ℂ closure(t).
LaTeX
$$$\\operatorname{frontier}(s \\times\\mathbb{C} t) = \\overline{s} \\times\\mathbb{C} \\operatorname{frontier}(t) \\cup \\operatorname{frontier}(s) \\times\\mathbb{C} \\overline{t}$$$
Lean4
theorem frontier_reProdIm (s t : Set ℝ) : frontier (s ×ℂ t) = closure s ×ℂ frontier t ∪ frontier s ×ℂ closure t := by
simpa only [← preimage_eq_preimage equivRealProdCLM.symm.toHomeomorph.surjective,
equivRealProdCLM.symm.toHomeomorph.preimage_frontier] using frontier_prod_eq s t
