R : Type u_1
M : Type u_2
M₂ : Type ?u.39830
M₃ : Type ?u.39833
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ comap (Submodule.subtype p) (p ⊓ p') ≤ comap (Submodule.subtype p) ((p ⊔ p') ⊓ p')
R : Type u_1
M : Type u_2
M₂ : Type ?u.39830
M₃ : Type ?u.39833
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ comap (Submodule.subtype p) (p ⊓ p') ≤ ker (subToSupQuotient p p')
rw [LinearMap.ker_comp, Submodule.ofLe, comap_codRestrict, ker_mkQ, map_comap_subtype]
no goals
R : Type u_1
M : Type u_2
M₂ : Type ?u.39830
M₃ : Type ?u.39833
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ comap (Submodule.subtype p) (p ⊓ p') ≤ comap (Submodule.subtype p) ((p ⊔ p') ⊓ p')
exact comap_mono (inf_le_inf_right _ le_sup_left)