Theorems · Definition · order theory

RightOrdContinuous

{α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → Prop

A function f between preorders is right order continuous if it preserves all infima of nonempty sets. We define it using IsGLB instead of sInf so that the proof works both for complete lattices and conditionally complete lattices.

Defined in

Mathlib.Order.OrdContinuous

Cited by

24 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

PreorderPreorder