English
The remainder of the Icc-based lemmas show that the monotonicity/relational properties preserve under the fundamental-interval framework, using CovariantClass and transitivity assumptions.
Русский
Остальные леммы на основе Icc показывают, что монотонность/отношения сохраняются в базовом интервале и распространяются с использованием ковариантности и транзитивности.
LaTeX
$$$\text{(Icc-based relations and monotonicity extend under appropriate covariant and transitive assumptions.)}$$$
Lean4
theorem strictMono_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) :
StrictMono f ↔ StrictMonoOn f (Icc l (l + a)) :=
⟨(StrictMono.strictMonoOn · _), AddConstMapClass.rel_map_of_Icc ha⟩
