ndinter_eq_zero_iff_disjoint

Mathlib.Data.Multiset.FinsetOps

URI: https://scilib.ai/kg/mathlib#Multiset.ndinter_eq_zero_iff_disjoint

English

ndinter s t equals zero exactly when s and t are disjoint.

Русский

ndinter s t = 0 тогда и только тогда, когда s и t несовместны (.disjoint).

LaTeX

$$ndinter s t = 0 \iff Disjoint s t$$

Lean4

theorem ndinter_eq_zero_iff_disjoint {s t : Multiset α} : ndinter s t = 0 ↔ Disjoint s t := by rw [← subset_zero];
  simp [subset_iff, disjoint_left]

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

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

Разделы

Аффилиация

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