interior_reProdIm — Mathlib

English

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

Русский

Для множеств s,t ⊆ ℝ: interior( s ×ℂ t ) = interior(s) ×ℂ interior(t).

LaTeX

$$$\\operatorname{interior}( s \\times\\mathbb{C} t) = \\operatorname{interior}(s) \\times\\mathbb{C} \\operatorname{interior}(t)$$$

Lean4

theorem interior_reProdIm (s t : Set ℝ) : interior (s ×ℂ t) = interior s ×ℂ interior t := by
  rw [reProdIm, reProdIm, interior_inter, interior_preimage_re, interior_preimage_im]

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