gc_map_comap

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

URI: https://scilib.ai/kg/mathlib#AffineSubspace.gc_map_comap

English

The same Galois connection statement: map f and comap f form a Galois connection.

Русский

Та же связь Гало: отображение map f и comap f образуют связь Гало.

LaTeX

$$$\\\\mathrm{GaloisConnection}(\\\\mathrm{map} f,\\\\mathrm{comap} f)$$$

Lean4

theorem gc_map_comap (f : P₁ →ᵃ[k] P₂) : GaloisConnection (map f) (comap f) := fun _ _ => map_le_iff_le_comap

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru