gc_map_comap — Mathlib

English

Let S be a submonoid of M and T a submonoid of N. For any morphism f, the operations map f and comap f form a Galois connection between submonoids: map f S is contained in T if and only if S is contained in comap f T.

Русский

Пусть S ⊆ M и T ⊆ N — подмоноиды. Тогда отображения map f и comap f образуют Галуа-связь: map f S ⊆ T тогда и только тогда S ⊆ comap f T.

LaTeX

$$$\forall S \in \operatorname{Submonoid}(M), \forall T \in \operatorname{Submonoid}(N),\; (\mathrm{map}\!\_f\,S) \le T \iff S \le (\mathrm{comap}\!\_f)\,T$$$

Lean4

@[to_additive]
theorem gc_map_comap (f : F) : GaloisConnection (map f) (comap f) := fun _ _ => map_le_iff_le_comap

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