map_inf — Mathlib

English

Under an injective map f, the image of S ∩ T equals the intersection of the images.

Русский

При инъективном отображении f образ пересечения S и T равен пересечению образов.

LaTeX

$$$ (f : F)\\; x \\text{ injective} \\implies (S \\cap T).map f = S.map f \\cap T.map f $$$

Lean4

theorem map_inf [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (hf : Function.Injective f)
    (S T : NonUnitalSubalgebra R A) : ((S ⊓ T).map f : NonUnitalSubalgebra R B) = S.map f ⊓ T.map f :=
  SetLike.coe_injective (Set.image_inter hf)

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