English
If f is injective, then the image of the intersection equals the intersection of the images: (p ∩ q).map f = (p.map f) ∩ (q.map f).
Русский
При инъективности отображения f образ пересечения равен пересечению образов: (p ∩ q).map f = (p.map f) ∩ (q.map f).
LaTeX
$$If injective f, then $(p \\cap q)\\ map\\ f = (p\\ map\\ f) \\cap (q\\ map\\ f)$$$
Lean4
theorem map_inf (f : F) {p q : Submodule R M} (hf : Injective f) : (p ⊓ q).map f = p.map f ⊓ q.map f :=
SetLike.coe_injective <| Set.image_inter hf