id — Mathlib · SciLib

English

The identity maps on α and α form a Galois connection: l = id and u = id satisfy the adjunction.

Русский

Тождественные отображения на α образуют связь Галуа: l = id и u = id удовлетворяют сопряжению.

LaTeX

$$$$ \text{GaloisConnection} (\mathrm{id}) (\mathrm{id}). $$$$

Lean4

protected theorem id [pα : Preorder α] : @GaloisConnection α α pα pα id id := fun _ _ =>
  Iff.intro (fun x => x) fun x => x

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