reProdIm — Mathlib

English

If s and t are bounded subsets of ℝ, then the complex prod s ×ℂ t is bounded in ℂ.

Русский

Если s и t ограничены в ℝ, то произведение s ×ℂ t ограничено в ℂ.

LaTeX

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

Lean4

theorem reProdIm (hs : IsBounded s) (ht : IsBounded t) : IsBounded (s ×ℂ t) :=
  antilipschitz_equivRealProd.isBounded_preimage (hs.prod ht)

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