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✝ = 0 ↔ ¬↑f a✝ = 0 ∧ ¬↑g a✝ = 0
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 [inf_apply, mem_support_iff, Ne.def, Finset.mem_inter]
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✝ = 0 ↔ ¬↑f a✝ = 0 ∧ ¬↑g a✝ = 0
simp only [inf_eq_min, ← nonpos_iff_eq_zero, min_le_iff, not_or]