comap_iSup_map_of_injective — Mathlib

English

If f is injective, the comap of the iSup of mapped submonoids equals the iSup of the original submonoids: comap f (iSup i (S i).map f) = iSup i S i.

Русский

Если f инъективен, то предобраз iSup образованных через f подмономиодов равен iSup исходных: comap f (iSup i (S i).map f) = iSup i S i.

LaTeX

$$$\mathrm{comap}\!\_f (\mathrm{iSup}\,i, (S_i).map\!\_f) = \mathrm{iSup}\,i, S_i$ (при инъективности f)$$

Lean4

@[to_additive]
theorem comap_iSup_map_of_injective (S : ι → Submonoid M) : (⨆ i, (S i).map f).comap f = iSup S :=
  (gciMapComap hf).u_iSup_l _

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