map_inf — Mathlib

English

If f is injective, image preserves infimum: map f (s ⊓ t) = map f s ⊓ map f t.

Русский

При инъективности отображение сохраняет инфимуум: map f (s ⊓ t) = map f s ⊓ map f t.

LaTeX

$$$\\big(\\forall f, \\ \\mathrm{Injective}(f) \\Rightarrow\\ (\\operatorname{map}_f(s \\cap t) = \\operatorname{map}_f(s) \\cap \\operatorname{map}_f(t))\\,)$$$

Lean4

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

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