mul_eq_empty — Mathlib

English

Let s and t be subsets of a set with a multiplicative structure. Then the product set s · t is empty if and only if at least one of s or t is empty.

Русский

Пусть s и t — подмножества множества с умножением. Тогда произведение множеств s · t пусто тогда и только тогда, когда хотя бы одно из множеств s или t пусто.

LaTeX

$$$s \cdot t = \emptyset \;\iff\; s = \emptyset \lor t = \emptyset$$$

Lean4

@[to_additive (attr := simp)]
theorem mul_eq_empty : s * t = ∅ ↔ s = ∅ ∨ t = ∅ :=
  image2_eq_empty_iff

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