mem_reProdIm — Mathlib

English

An element z belongs to s ×ℂ t exactly when Re(z) ∈ s and Im(z) ∈ t.

Русский

Элемент z принадлежит s ×ℂ t тогда и только тогда, когда Re(z) ∈ s и Im(z) ∈ t.

LaTeX

$$$\\\\forall z \\\\in \\\\mathbb{C}, \\\\forall s,t \\\\subseteq \\\\mathbb{R}, \\\\; z \\\\in s \\\\times\\\\!_\\!\\\\! t \iff \\\\operatorname{Re}(z) \\\\in s \\\\land \\\\operatorname{Im}(z) \\\\in t.$$$

Lean4

theorem mem_reProdIm {z : ℂ} {s t : Set ℝ} : z ∈ s ×ℂ t ↔ z.re ∈ s ∧ z.im ∈ t :=
  Iff.rfl

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