preimage_equivRealProd_prod — Mathlib

English

For s,t ⊆ ℝ, the preimage of s × t under the real–complex equivalence equals s ×ℂ t.

Русский

Для подмножеств s,t ⊆ ℝ прообраз под отображением эквивалентности действительных чисел и комплексных чисел от s × t равен s ×ℂ t.

LaTeX

$$$(\\mathrm{equivRealProd})^{-1}(s \\times t) = s \\times_{\\mathbb{C}} t$$$

Lean4

/-- The preimage under `equivRealProd` of `s ×ˢ t` is `s ×ℂ t`. -/
theorem preimage_equivRealProd_prod (s t : Set ℝ) : equivRealProd ⁻¹' (s ×ˢ t) = s ×ℂ t :=
  rfl

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