to_galoisConnection — Mathlib

English

If e is an order isomorphism α ≃o β, then e and its inverse e^{-1} form a Galois connection: for all a,b one has a ≤ e(b) iff e^{-1}(a) ≤ b.

Русский

Если e — упорядоченная биекция α ≃o β, то пары e и e^{-1} образуют связь Галуа: для всех a,b выполняется a ≤ e(b) эквивалентно e^{-1}(a) ≤ b.

LaTeX

$$$$ GaloisConnection\, e\, e^{-1}. $$$$

Lean4

/-- Makes a Galois connection from an order-preserving bijection. -/
theorem to_galoisConnection (e : α ≃o β) : GaloisConnection e e.symm := fun _ _ => e.rel_symm_apply.symm

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