case h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x✝ x : (i : ι) → φ i
⊢ (x ∈ ⨅ (i : ι) (_ : i ∈ I), comap (proj i) (p i)) ↔ x ∈ pi I p
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
⊢ (⨅ (i : ι) (_ : i ∈ I), comap (proj i) (p i)) = pi I p
ext x
no goals
case h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x✝ x : (i : ι) → φ i
⊢ (x ∈ ⨅ (i : ι) (_ : i ∈ I), comap (proj i) (p i)) ↔ x ∈ pi I p
simp