English
A function between locally finite preorders is monotone iff it preserves order for all pairs related by the weak cover relation WCovBy.
Русский
Функция между локально конечными предуровнями монотонна тогда и только тогда, когда она сохраняет порядок для всех пар, связанных отношением WCovBy.
LaTeX
$$$\text{Monotone}(f) \iff \forall a,b, \mathrm{WCovBy}(a,b) \rightarrow f(a) \le f(b)$$$
Lean4
/-- A function from a locally finite preorder is monotone if and only if it is monotone when
restricted to pairs satisfying `a ⩿ b`. -/
theorem monotone_iff_forall_wcovBy [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) :
Monotone f ↔ ∀ a b : α, a ⩿ b → f a ≤ f b :=
by
refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩
simpa [transGen_eq_self (r := (· ≤ · : β → β → Prop)) transitive_le] using
TransGen.lift f h <| le_iff_transGen_wcovBy.mp hab
