vsub_eq_empty — Mathlib

English

The vsub is empty exactly when one of the sets is empty: s −ᵥ t = ∅ iff s = ∅ or t = ∅.

Русский

Разность по векторному вычитанию пуста тогда и только тогда, когда одно из множеств пусто: s −ᵥ t = ∅ ↔ s = ∅ или t = ∅.

LaTeX

$$$ s -ᵥ t = ∅ \iff s = ∅ \lor t = ∅ $$$

Lean4

@[simp]
theorem vsub_eq_empty : s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅ :=
  image2_eq_empty_iff

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