prod_nonempty_iff — Mathlib

English

Let S ⊆ α and T ⊆ β be sets. Then S × T is nonempty if and only if both S and T are nonempty.

Русский

Пусть S ⊆ α и T ⊆ β. Тогда S × T непусто тогда и только тогда, когда S непусто и T непусто.

LaTeX

$$$ (s \times t) \neq \emptyset \;\iff\; s \neq \emptyset \land t \neq \emptyset $$$

Lean4

@[simp]
theorem prod_nonempty_iff : (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty :=
  ⟨fun h => ⟨h.fst, h.snd⟩, fun h => h.1.prod h.2⟩

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