div_eq_empty — Mathlib

English

The division s / t is empty precisely when either s or t is empty: s / t = ∅ iff s = ∅ or t = ∅.

Русский

Деление s / t пусто тогда и только тогда, когда хотя бы одно из множеств s или t пусто: s / t = ∅ ⇔ s = ∅ или t = ∅.

LaTeX

$$$ s / t = \emptyset \iff s = \emptyset \lor t = \emptyset $$$

Lean4

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

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