no goals
α : Type u_2
M : Type u_3
N : Type ?u.111089
P : Type ?u.111092
R : Type u_4
S : Type ?u.111098
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_1
s : ι → Set α
x : α →₀ M
⊢ x ∈ supported M R (⋂ (i : ι), s i) ↔ x ∈ ⨅ (i : ι), supported M R (s i)
simp [mem_supported, subset_iInter_iff]