map_inf — Mathlib

English

If f is injective, then the map of the infimum equals the infimum of the maps: (S ⊓ T).map f = S.map f ⊓ T.map f.

Русский

Если отображение инъективно, то образ пересечения равно пересечению образов: (S ∩ T).map f = S.map f ∩ T.map f.

LaTeX

$$(S ⊓ T).map f = S.map f ⊓ T.map f$$

Lean4

@[to_additive]
theorem map_inf (S T : Subsemigroup M) (f : M →ₙ* N) (hf : Function.Injective f) : (S ⊓ T).map f = S.map f ⊓ T.map f :=
  SetLike.coe_injective (Set.image_inter hf)

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