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