toGaloisInsertion — Mathlib

English

From an order isomorphism e, one obtains a GaloisInsertion e e^{-1}, where choice, gc, and the unit-counit relations are given by e.

Русский

Из упорядоченной изоморфии e следует GaloisInsertion e e^{-1}, где выбор функции, связь Галуа и соответствия задаются через e.

LaTeX

$$$$ \\text{GaloisInsertion}(e,e^{-1}). $$$$

Lean4

/-- Makes a Galois insertion from an order-preserving bijection. -/
protected def toGaloisInsertion (e : α ≃o β) : GaloisInsertion e e.symm
    where
  choice b _ := e b
  gc := e.to_galoisConnection
  le_l_u g := le_of_eq (e.right_inv g).symm
  choice_eq _ _ := rfl

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