map_inf — Mathlib

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

Похожие утверждения