English
Let α be a locally finite order and β a preorder. A function f: α → β is strictly monotone iff it is strictly monotone 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, выполняется неравенство f(a) < f(b).
LaTeX
$$$\operatorname{StrictMono}(f) \iff \forall a,b\in \alpha\, (a \prec b) \Rightarrow f(a) < f(b)$$$
Lean4
/-- A function from a locally finite preorder is strictly monotone if and only if it is strictly
monotone when restricted to pairs satisfying `a ⋖ b`. -/
theorem strictMono_iff_forall_covBy [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) :
StrictMono f ↔ ∀ a b : α, a ⋖ b → f a < f b :=
by
refine ⟨fun hf _ _ h ↦ hf h.lt, fun h a b hab ↦ ?_⟩
have := Relation.TransGen.lift f h (a := a) (b := b)
rw [← lt_iff_transGen_covBy, transGen_eq_self (@lt_trans β _)] at this
exact this hab
