ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ support f ∩ support g = ∅ ↔ support f ⊓ support g = ⊥
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ Disjoint f g ↔ Disjoint (support f) (support g)
rw [disjoint_iff, disjoint_iff, Dfinsupp.bot_eq_zero, ← Dfinsupp.support_eq_empty,
  Dfinsupp.support_inf]
no goals
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ support f ∩ support g = ∅ ↔ support f ⊓ support g = ⊥
rfl