gc_map_comap — Mathlib

English

The pair of operations map f and comap f form a Galois connection on Lie ideals: map f is left adjoint to comap f.

Русский

Пусть пары операций map f и comap f образуют связь Галуа на Ли-идеалах: map f является левым соседствующим отображением к comap f.

LaTeX

$$GaloisConnection (map f) (comap f)$$

Lean4

theorem gc_map_comap : GaloisConnection (map f) (comap f) := fun _ _ ↦ map_le_iff_le_comap

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