map_inf — Mathlib

English

For subrings s,t of R and an injective f, 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\\bigl(s \\sqcap t\\bigr) = \\mathrm{map}\,f(s) \\sqcap \\mathrm{map}\\,f(t)$$$

Lean4

theorem map_inf (s t : Subring 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)

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