map_comap_le — Mathlib

English

Let f be a ring homomorphism-like structure and K an ideal on the codomain. Then the image of the preimage of K under f is contained in K, i.e. map f (comap f K) ≤ K.

Русский

Пусть f—непрерывное отображение колец и K — идеал кодоменого множества. Тогда образ прообраза K через f содержится в K, т.е. map f (comap f K) ≤ K.

LaTeX

$$$\\operatorname{map} f\\bigl(\\operatorname{comap} f(K)\\bigr) \\le K$$$

Lean4

theorem map_comap_le : (K.comap f).map f ≤ K :=
  (gc_map_comap f).l_u_le _

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