vsub_eq_empty

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

URI: https://scilib.ai/kg/mathlib#Finset.vsub_eq_empty

English

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

Русский

vsub пустой тогда и только тогда, когда хотя бы одно из с и т пусто.

LaTeX

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

Lean4

@[simp]
theorem vsub_eq_empty : s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅ :=
  image₂_eq_empty_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru