map_inf — Mathlib

English

Let f be as above and injective. Then the image of the infimum equals the infimum of the images: (S ⊓ T).map f = S.map f ⊓ T.map f.

Русский

Пусть f инъективен. Тогда образ пересечения равен пересечению образов: (S ⊓ T).map f = S.map f ⊓ T.map f.

LaTeX

$$$(S \\cap T).map f = S.map f \\cap T.map f$$$

Lean4

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

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