R : Type u_2
R₂ : Type ?u.224705
K : Type ?u.224708
M : Type u_1
M₂ : Type ?u.224714
V : Type ?u.224717
S✝ : Type ?u.224720
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
S : Finset M
⊢ CompleteLattice.IsCompactElement (⨆ (x : M) (_ : x ∈ ↑S), span R {x})
R : Type u_2
R₂ : Type ?u.224705
K : Type ?u.224708
M : Type u_1
M₂ : Type ?u.224714
V : Type ?u.224717
S✝ : Type ?u.224720
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
S : Finset M
⊢ CompleteLattice.IsCompactElement (span R ↑S)
rw [span_eq_iSup_of_singleton_spans]
R : Type u_2
R₂ : Type ?u.224705
K : Type ?u.224708
M : Type u_1
M₂ : Type ?u.224714
V : Type ?u.224717
S✝ : Type ?u.224720
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
S : Finset M
⊢ CompleteLattice.IsCompactElement (⨆ (x : M) (_ : x ∈ S), span R {x})
R : Type u_2
R₂ : Type ?u.224705
K : Type ?u.224708
M : Type u_1
M₂ : Type ?u.224714
V : Type ?u.224717
S✝ : Type ?u.224720
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
S : Finset M
⊢ CompleteLattice.IsCompactElement (⨆ (x : M) (_ : x ∈ ↑S), span R {x})
simp only [Finset.mem_coe]
R : Type u_2
R₂ : Type ?u.224705
K : Type ?u.224708
M : Type u_1
M₂ : Type ?u.224714
V : Type ?u.224717
S✝ : Type ?u.224720
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
S : Finset M
⊢ CompleteLattice.IsCompactElement (Finset.sup S fun x => span R {x})
R : Type u_2
R₂ : Type ?u.224705
K : Type ?u.224708
M : Type u_1
M₂ : Type ?u.224714
V : Type ?u.224717
S✝ : Type ?u.224720
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
S : Finset M
⊢ CompleteLattice.IsCompactElement (⨆ (x : M) (_ : x ∈ S), span R {x})
rw [← Finset.sup_eq_iSup]
no goals
R : Type u_2
R₂ : Type ?u.224705
K : Type ?u.224708
M : Type u_1
M₂ : Type ?u.224714
V : Type ?u.224717
S✝ : Type ?u.224720
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
S : Finset M
⊢ CompleteLattice.IsCompactElement (Finset.sup S fun x => span R {x})
exact
  CompleteLattice.finset_sup_compact_of_compact S fun x _ => singleton_span_isCompactElement x