English
RightOrdContinuous f is the property that f preserves infima: whenever s ⊆ α has x as a greatest lower bound, f''s has f x as a greatest lower bound.
Русский
RightOrdContinuous f означает, что f сохраняет Infima: если x — наибольшая общая нижняя грань множества s, то f''s имеет f x как общую нижнюю грань.
LaTeX
$$$\mathrm{RightOrdContinuous}(f) := \forall s,x,\ IsGLB(s,x) \rightarrow IsGLB(f''s, f x)$$$
Lean4
/-- A function `f` between preorders is right order continuous if it preserves all infima. We
define it using `IsGLB` instead of `sInf` so that the proof works both for complete lattices and
conditionally complete lattices. -/
def RightOrdContinuous [Preorder α] [Preorder β] (f : α → β) :=
∀ ⦃s : Set α⦄ ⦃x⦄, IsGLB s x → IsGLB (f '' s) (f x)
