English
For G additive group with a>0 and H additive group, an AddConstMap f is monotone iff it is monotone on the closed interval Icc(l, l+a) for any l.
Русский
Для любой непустой области добавления элемент f монотонна тогда и только тогда, когда она монотонна на замкнутом промежутке Icc(l, l+a) для любого l.
LaTeX
$$$\text{Monotone}(f) \iff \text{MonotoneOn}(f, Icc(l, l+a))$.$$
Lean4
theorem monotone_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [AddCommGroup H]
[PartialOrder H] [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :
Monotone f ↔ MonotoneOn f (Icc l (l + a)) :=
⟨(Monotone.monotoneOn · _), fun hf ↦
monotone_iff_forall_lt.2 <| AddConstMapClass.rel_map_of_Icc ha fun _x hx _y hy hxy ↦ hf hx hy hxy.le⟩
