closure_reProdIm — Mathlib

English

For sets s,t ⊆ ℝ, the closure of the complex prod s ×ℂ t equals the prod of closures: closure(s ×ℂ t) = closure(s) ×ℂ closure(t).

Русский

Для множеств s,t ⊆ ℝ выполняется: замыкание( s ×ℂ t ) = замыкание(s) ×ℂ замыкание(t).

LaTeX

$$$\\overline{\,s \\times\\!\\mathbb{C} \\! t\\} = \\overline{s} \\times\\!\\mathbb{C} \\overline{t}$$$

Lean4

theorem closure_reProdIm (s t : Set ℝ) : closure (s ×ℂ t) = closure s ×ℂ closure t := by
  simpa only [← preimage_eq_preimage equivRealProdCLM.symm.toHomeomorph.surjective,
    equivRealProdCLM.symm.toHomeomorph.preimage_closure] using @closure_prod_eq _ _ _ _ s t

Похожие утверждения