le_comap_map — Mathlib

English

For any filter f on α and map m: α → β, pulling back along m and then re-applying m yields a relation that contains f: f ≤ comap m (map m f).

Русский

Для любого фильтра f на α и отображения m: α → β последовательность «обратного изображения» и затем прямого отображения даёт: f ≤ comap m (map m f).

LaTeX

$$$ f \\le \\operatorname{comap}_m(\\operatorname{map}_m f) $$$

Lean4

theorem le_comap_map : f ≤ comap m (map m f) :=
  (gc_map_comap m).le_u_l _

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