gc_map_comap — Mathlib

English

The pair (map m, comap m) forms a Galois connection; i.e., the map is left adjoint to comap in the filter order.

Русский

Пара (map m, comap m) образует сопряжённость Гало; то есть map является левым сопряжённым по отношению к comap в порядке фильтров.

LaTeX

$$$\\text{gc_map_comap}\\ (m)$ expresses a Galois connection between (map m) and (comap m).$$

Lean4

theorem gc_map_comap (m : α → β) : GaloisConnection (map m) (comap m) := fun _ _ => map_le_iff_le_comap

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