reProdIm_subset_iff — Mathlib

English

For subsets s,s1,t,t1 ⊆ ℝ, s ×ℂ t ⊆ s1 ×ℂ t1 if and only if s × t ⊆ s1 × t1.

Русский

Для подмножеств s,s1,t,t1 ⊆ ℝ верно: s ×ℂ t ⊆ s1 ×ℂ t1 тогда и только тогда, когда s × t ⊆ s1 × t1.

LaTeX

$$$s \\times_\\mathbb{C} t \\subseteq s_1 \\times_\\mathbb{C} t_1 \\quad\\text{iff}\\quad s \\times t \\subseteq s_1 \\times t_1$$$

Lean4

/-- The inequality `s × t ⊆ s₁ × t₁` holds in `ℂ` iff it holds in `ℝ × ℝ`. -/
theorem reProdIm_subset_iff {s s₁ t t₁ : Set ℝ} : s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁ :=
  by
  rw [← @preimage_equivRealProd_prod s t, ← @preimage_equivRealProd_prod s₁ t₁]
  exact Equiv.preimage_subset equivRealProd _ _

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