reProdIm_eq_empty — Mathlib

English

The product s ×ℂ t equals the empty set if and only if s = ∅ or t = ∅.

Русский

Произведение s ×ℂ t равно пустому множеству тогда и только тогда, когда s = ∅ или t = ∅.

LaTeX

$$$s \\times_\\mathbb{C} t = \\emptyset \\iff s = \\emptyset \\lor t = \\emptyset$$$

Lean4

@[simp]
theorem reProdIm_eq_empty : s ×ℂ t = ∅ ↔ s = ∅ ∨ t = ∅ := by
  simp [← not_nonempty_iff_eq_empty, reProdIm_nonempty, -not_and, not_and_or]

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