gc_top_lie_normalizer — Mathlib

English

The pair of maps N ↦ [⊤, N] and N ↦ N.normalizer forms a Galois connection between LieSubmodules.

Русский

Пара отображений N ↦ [⊤, N] и N ↦ N.normalizer образует Галуа-отношение между Ли-подмодулями.

LaTeX

$$$ \\text{GaloisConnection}\\left(\\lambda N. [\\top, N],\\ \\lambda N. N.normalizer\\right)$$$

Lean4

theorem gc_top_lie_normalizer : GaloisConnection (fun N : LieSubmodule R L M => ⁅(⊤ : LieIdeal R L), N⁆) normalizer :=
  top_lie_le_iff_le_normalizer

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