no goals
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyLinearOrderedAddMonoid α
f g : ι →₀ α
⊢ Disjoint f g ↔ Disjoint f.support g.support
classical
  rw [disjoint_iff, disjoint_iff, Finsupp.bot_eq_zero, ← Finsupp.support_eq_empty,
    Finsupp.support_inf]
  rfl
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyLinearOrderedAddMonoid α
f g : ι →₀ α
⊢ f.support ∩ g.support = ∅ ↔ f.support ⊓ g.support = ⊥
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyLinearOrderedAddMonoid α
f g : ι →₀ α
⊢ Disjoint f g ↔ Disjoint f.support g.support
rw [disjoint_iff, disjoint_iff, Finsupp.bot_eq_zero, ← Finsupp.support_eq_empty,
  Finsupp.support_inf]
no goals
ι : Type u_1
α : Type u_2
inst✝ : CanonicallyLinearOrderedAddMonoid α
f g : ι →₀ α
⊢ f.support ∩ g.support = ∅ ↔ f.support ⊓ g.support = ⊥
rfl