reProdIm — Mathlib

English

If s and t are open subsets of ℝ, then the set { x+iy : x ∈ s, y ∈ t } is open in ℂ.

Русский

Если s и t открыты в ℝ, то множество { x+iy : x ∈ s, y ∈ t } открыто в ℂ.

LaTeX

$$$\\text{IsOpen}(s) \\land \\text{IsOpen}(t) \\Rightarrow \\text{IsOpen}(\\operatorname{reProdIm}(s,t))$$$

Lean4

theorem reProdIm (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ×ℂ t) :=
  (hs.preimage continuous_re).inter (ht.preimage continuous_im)

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