case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ a✝ ∈ support (f ⊔ g) ↔ a✝ ∈ support f ∪ support g
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ support (f ⊔ g) = support f ∪ support g
ext
case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ ¬↑f a✝ ⊔ ↑g a✝ = ⊥ ↔ ¬↑f a✝ = ⊥ ∨ ¬↑g a✝ = ⊥
case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ a✝ ∈ support (f ⊔ g) ↔ a✝ ∈ support f ∪ support g
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✝¹ : (i : ι) → CanonicallyLinearOrderedAddMonoid (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ ¬↑f a✝ ⊔ ↑g a✝ = ⊥ ↔ ¬↑f a✝ = ⊥ ∨ ¬↑g a✝ = ⊥
rw [_root_.sup_eq_bot_iff, not_and_or]