inter_eq_zero_iff_disjoint — Mathlib

English

For multisets s,t with decidable equality, s ∩ t = 0 if and only if Disjoint s t.

Русский

Для мультисетов s,t с определяемостью равенства, s ∩ t = 0 тогда и только тогда, когда s и t несовместны.

LaTeX

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

Lean4

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

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