reProdIm_nonempty

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.reProdIm_nonempty

English

The rectangle s ×ℂ t is nonempty if and only if s and t are both nonempty.

Русский

Прямоугольник s ×ℂ t непуст, если и только если s и t непусты.

LaTeX

$$$(s \\times_\\mathbb{C} t).\\mathrm{Nonempty} \\iff s.Nonempty \\land t.Nonempty$$$

Lean4

@[simp]
theorem reProdIm_nonempty : (s ×ℂ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := by
  simp [Set.Nonempty, reProdIm, Complex.exists]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru