English
Let α be a locally finite partial order and β a preorder. A function f: α → β is monotone if and only if it preserves the order on all cover relations, i.e. for every a,b ∈ α with a covered by b, we have f(a) ≤ f(b).
Русский
Пусть α — локально конечный частичный порядок, β — предпорядок. Функция f: α → β монотонна тогда и только тогда, когда для каждой пары a,b ∈ α, где a покрывается b (a ⋖ b), выполняется неравенство f(a) ≤ f(b).
LaTeX
$$$\operatorname{Monotone}(f) \Longleftrightarrow \forall a,b\in \alpha\, (a \prec b) \Rightarrow f(a) \le f(b)$$$
Lean4
/-- A function from a locally finite partial order is monotone if and only if it is monotone when
restricted to pairs satisfying `a ⋖ b`. -/
theorem monotone_iff_forall_covBy [PartialOrder α] [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 [reflTransGen_eq_self (r := (· ≤ · : β → β → Prop)) IsRefl.reflexive transitive_le] using
ReflTransGen.lift f h <| le_iff_reflTransGen_covBy.mp hab
