diffs_eq_empty — Mathlib

English

For finite sets s and t, the set of all pairwise differences {a \\ b | a ∈ s, b ∈ t} is empty if and only if s = ∅ or t = ∅.

Русский

Для конечных множеств s и t множество всех различий {a \\ b | a ∈ s, b ∈ t} пусто тогда и только тогда, когда s = ∅ или t = ∅.

LaTeX

$$$ s \\ diffs t = \\emptyset \\;\\;\\Longleftrightarrow \\;\\; s = \\emptyset \\;\\lor\\; t = \\emptyset $$$

Lean4

@[simp]
theorem diffs_eq_empty : s \\ t = ∅ ↔ s = ∅ ∨ t = ∅ :=
  image₂_eq_empty_iff

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