reProdIm_subset_iff' — Mathlib

English

If s ⊆ s1 ⊆ ℝ and t ⊆ t1 ⊆ ℝ, then s ×ℂ t ⊆ s1 ×ℂ t1 if and only if (s ⊆ s1 ∧ t ⊆ t1) or s = ∅ or t = ∅.

Русский

Если s ⊆ s1 ⊆ ℝ и t ⊆ t1 ⊆ ℝ, то s ×ℂ t ⊆ s1 ×ℂ t1 тогда и только тогда, когда (s ⊆ s1 и t ⊆ t1) или s = ∅ или t = ∅.

LaTeX

$$$s \\times_\\mathbb{C} t \\subseteq s_1 \\times_\\mathbb{C} t_1 \\iff (s \\subseteq s_1 \\land t \\subseteq t_1) \\lor s = \\emptyset \\lor t = \\emptyset$$$

Lean4

/-- If `s ⊆ s₁ ⊆ ℝ` and `t ⊆ t₁ ⊆ ℝ`, then `s × t ⊆ s₁ × t₁` in `ℂ`. -/
theorem reProdIm_subset_iff' {s s₁ t t₁ : Set ℝ} : s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ :=
  by
  convert prod_subset_prod_iff
  exact reProdIm_subset_iff

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