R : Type u_1
R₂ : Type u_2
K : Type ?u.14881
M : Type u_3
M₂ : Type u_4
V : Type ?u.14890
S : Type ?u.14893
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
f : M →ₛₗ[σ₁₂] M₂
s : Set M₂
⊢ ↑f ⁻¹' s ⊆ ↑f ⁻¹' ↑(span R₂ s)
R : Type u_1
R₂ : Type u_2
K : Type ?u.14881
M : Type u_3
M₂ : Type u_4
V : Type ?u.14890
S : Type ?u.14893
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
f : M →ₛₗ[σ₁₂] M₂
s : Set M₂
⊢ span R (↑f ⁻¹' s) ≤ comap f (span R₂ s)
rw [span_le, comap_coe]
no goals
R : Type u_1
R₂ : Type u_2
K : Type ?u.14881
M : Type u_3
M₂ : Type u_4
V : Type ?u.14890
S : Type ?u.14893
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
f : M →ₛₗ[σ₁₂] M₂
s : Set M₂
⊢ ↑f ⁻¹' s ⊆ ↑f ⁻¹' ↑(span R₂ s)
exact preimage_mono subset_span