comap_iInf_map_of_injective — Mathlib

English

If f is injective, comap f distributes over infimum of images: comap f (map f S ∧ map f T) = S ∧ T.

Русский

При инъекции f, предобраз через f распределяется по инфиминуму образов: comap f (map f S ∧ map f T) = S ∧ T.

LaTeX

$$$\mathrm{comap}\!\_f(\mathrm{min}(\mathrm{map}\!\_f S, \mathrm{map}\!\_f T)) = \mathrm{min}(S, T)$ (при инъективности f)$$

Lean4

@[to_additive]
theorem comap_iInf_map_of_injective (S : ι → Submonoid M) : (⨅ i, (S i).map f).comap f = iInf S :=
  (gciMapComap hf).u_iInf_l _

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