map_inf — Mathlib

English

If f is injective, then the image of the intersection equals the intersection of the images: (N ⊓ N₂).map f = N.map f ⊓ N₂.map f.

Русский

Если f инъективен, то образ пересечения равен пересечению образов: (N ∩ N₂).map f = N.map f ∩ N₂.map f.

LaTeX

$$((N \\cap N_2).map f) = (N.map f) \\cap (N_2.map f)$$

Lean4

theorem map_inf (hf : Function.Injective f) : (N ⊓ N₂).map f = N.map f ⊓ N₂.map f :=
  SetLike.coe_injective <| Set.image_inter hf

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