case a
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ a✝ ∈ (f ⊔ g).support ↔ a✝ ∈ f.support ∪ g.support
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊔ g).support = f.support ∪ g.support
ext
case a
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ ¬↑f a✝ ⊔ ↑g a✝ = ⊥ ↔ ¬↑f a✝ = ⊥ ∨ ¬↑g a✝ = ⊥
case a
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ a✝ ∈ (f ⊔ g).support ↔ a✝ ∈ f.support ∪ g.support
simp only [Finset.mem_union, mem_support_iff, sup_apply, Ne.def, ← bot_eq_zero]
no goals
case a
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyLinearOrderedAddMonoid α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ ¬↑f a✝ ⊔ ↑g a✝ = ⊥ ↔ ¬↑f a✝ = ⊥ ∨ ¬↑g a✝ = ⊥
rw [_root_.sup_eq_bot_iff, not_and_or]