case a
α : Type ?u.12121
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) ≤ -span R s

case a
α : Type ?u.12121
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -span R s ≤ span R (-s)
α : Type ?u.12121
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) = -span R s
apply le_antisymm
case a
α : Type ?u.12121
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ s ⊆ ↑(span R s)
case a
α : Type ?u.12121
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) ≤ -span R s
rw [span_le, coe_set_neg, ← Set.neg_subset, neg_neg]
no goals
case a
α : Type ?u.12121
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ s ⊆ ↑(span R s)
exact subset_span
case a
α : Type ?u.12121
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -s ⊆ ↑(span R (-s))
case a
α : Type ?u.12121
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -span R s ≤ span R (-s)
rw [neg_le, span_le, coe_set_neg, ← Set.neg_subset]
no goals
case a
α : Type ?u.12121
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -s ⊆ ↑(span R (-s))
exact subset_span