leftOrdContinuous — Mathlib

English

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

Русский

Левый сопряженный в отношениях Галуа является слева непрерывным в порядковом смысле.

LaTeX

$$$ \\text{LeftOrdContinuous}(f) \\quad\\text{for } f \\text{ part of a Galois connection } f \\dashv g. $$$

Lean4

/-- A left adjoint in a Galois connection is left-continuous in the order-theoretic sense. -/
theorem leftOrdContinuous (gc : GaloisConnection f g) : LeftOrdContinuous f := fun _ _ ↦ gc.isLUB_l_image

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