giRestrict — Mathlib

English

The restriction of a nucleus to its range forms a Galois insertion with the forgetful map from the range to the original frame.

Русский

Ограничение ядра до диапазона образует Галуа-инсерцию с забывающим отображением из диапазона в исходную раму.

LaTeX

$$$\\mathrm{giRestrict}(n) : \\mathrm{GaloisInsertion}\\big(n\\restriction, \\mathrm{Subtype}.\\mathrm{val}\\big)$$$

Lean4

/-- The restriction of a nucleus to its range forms a Galois insertion with the forgetful map from
the range to the original frame. -/
def giRestrict (n : Nucleus X) : GaloisInsertion n.restrict Subtype.val :=
  n.giAux

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