map_inf — Mathlib

English

If f is injective, the image of the infimum equals the infimum of the images: map f (s ⊓ t) = map f s ⊓ map f t.

Русский

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

LaTeX

$$$\\mathrm{map}\ f\\,(s \\wedge t) = \\mathrm{map}\ f\\ s \\wedge \\mathrm{map}\ f\\ t$ (при инъекции $f$)$$

Lean4

theorem map_inf (s t : Subsemiring R) (f : R →+* S) (hf : Function.Injective f) : (s ⊓ t).map f = s.map f ⊓ t.map f :=
  SetLike.coe_injective (Set.image_inter hf)

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