α : Type u_1
inst✝ : DecidableEq α
s✝ s t : Multiset α
⊢ ndinter s t ⊆ 0 ↔ Disjoint s t
α : Type u_1
inst✝ : DecidableEq α
s✝ s t : Multiset α
⊢ ndinter s t = 0 ↔ Disjoint s t
rw [← subset_zero]
no goals
α : Type u_1
inst✝ : DecidableEq α
s✝ s t : Multiset α
⊢ ndinter s t ⊆ 0 ↔ Disjoint s t
simp [subset_iff, Disjoint]