comap_inf — Mathlib

English

The comap distributes over infimum: (S ⊓ T).comap f = S.comap f ⊓ T.comap f.

Русский

Предобраз распределяется по инфиминуму: (S ⊓ T).comap f = S.comap f ⊓ T.comap f.

LaTeX

$$$ (S \cap T).{\mathrm{comap}}\!\_f = S.{\mathrm{comap}}\!\_f \cap T.{\mathrm{comap}}\!\_f$$$

Lean4

@[to_additive]
theorem comap_inf (S T : Submonoid N) (f : F) : (S ⊓ T).comap f = S.comap f ⊓ T.comap f :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).u_inf

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