map_inf — Mathlib

English

The image of an infimum under an injective map is the infimum of the images: (s ⊓ t).map f = s.map f ⊓ t.map f, provided f is injective.

Русский

Образ наименьшего общего множителя при инъективном отображении равен наименьшему общему множителю образов: (s ⊓ t).map f = s.map f ⊓ t.map f, если f инъективно.

LaTeX

$$$ (s \\cap t).map\\; f = s.map\\; f \\cap t.map\\; f $ при условии $\\text{Function.Injective } f$$$

Lean4

theorem map_inf (s t : NonUnitalSubring R) (f : F) (hf : Function.Injective f) : (s ⊓ t).map f = s.map f ⊓ t.map f :=
  SetLike.coe_injective (Set.image_inter hf)

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