giRestrict — Mathlib

English

The restriction corresponding to a sublocale forms a Galois insertion with the forgetful map from the sublocale to the original locale.

Русский

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

LaTeX

$$$\mathrm{giRestrict}(S) : \mathrm{GaloisInsertion}(S.restrict, \mathrm{Subtype.val})$$$

Lean4

/-- The restriction corresponding to a sublocale forms a Galois insertion with the forgetful map
from the sublocale to the original locale. -/
def giRestrict (S : Sublocale X) : GaloisInsertion S.restrict Subtype.val :=
  S.giAux

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