R : Type u_2
R₂ : Type ?u.237748
K : Type ?u.237751
M : Type u_3
M₂ : Type ?u.237757
V : Type ?u.237760
S : Type ?u.237763
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
m : M
⊢ (∀ (b : Submodule R M), (∀ (i : ι), p i ≤ b) → span R {m} ≤ b) ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
R : Type u_2
R₂ : Type ?u.237748
K : Type ?u.237751
M : Type u_3
M₂ : Type ?u.237757
V : Type ?u.237760
S : Type ?u.237763
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
m : M
⊢ (m ∈ ⨆ (i : ι), p i) ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
rw [← span_singleton_le_iff_mem, le_iSup_iff]
no goals
R : Type u_2
R₂ : Type ?u.237748
K : Type ?u.237751
M : Type u_3
M₂ : Type ?u.237757
V : Type ?u.237760
S : Type ?u.237763
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
m : M
⊢ (∀ (b : Submodule R M), (∀ (i : ι), p i ≤ b) → span R {m} ≤ b) ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
simp only [span_singleton_le_iff_mem]