rightOrdContinuous — Mathlib

English

A right adjoint in a Galois connection is right-continuous in the order-theoretic sense.

Русский

Правый сопряженный в отношении Галуа является правой непрерывностью порядка.

LaTeX

$$$ \\text{RightOrdContinuous}(g) \\text{ for } g \\text{ in a Galois connection } f \\dashv g. $$$

Lean4

/-- A right adjoint in a Galois connection is right-continuous in the order-theoretic sense. -/
theorem rightOrdContinuous (gc : GaloisConnection f g) : RightOrdContinuous g := fun _ _ ↦ gc.isGLB_u_image

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