gc_comap_kernMap — Mathlib

English

The pair (comap m, kernMap m) forms a Galois connection; i.e., for any filters F,G on β, F ≤ G implies comap m F ≤ comap m G implies kernMap m F ≤ kernMap m G, establishing a standard adjunction.

Русский

Пара (comap m, kernMap m) образует сопряжённость Гало; то есть для любых фильтров F,G на β, F ≤ G влечёт comap m F ≤ comap m G, и наоборот.

LaTeX

$$$\\text{GaloisConnection}(\\mathrm{comap}\\ m, \\mathrm{kernMap}\\ m)$$$

Lean4

theorem gc_comap_kernMap (m : α → β) : GaloisConnection (comap m) (kernMap m) := fun _ _ ↦ comap_le_iff_le_kernMap

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