English
If f1 and f2 are pointwise equal on s, then monotonicity on s of f1 is equivalent to monotonicity on s of f2.
Русский
Если f1 и f2 совпадают на области s точка по точке, то монотонность на s f1 эквивалентна монотонности на s f2.
LaTeX
$$$\\forall {\\alpha \\beta \\gamma},\\ s: Set\\alpha,\\ f_1,f_2: \\alpha \\to \\beta,\\ [Preorder\\alpha][Preorder\\beta]\\n( h_1 : \\operatorname{MonotoneOn} f_1 s ) \\to ( s.EqOn f_1 f_2 s ) \\to \\operatorname{MonotoneOn} f_2 s$$$
Lean4
theorem _root_.MonotoneOn.congr (h₁ : MonotoneOn f₁ s) (h : s.EqOn f₁ f₂) : MonotoneOn f₂ s :=
by
intro a ha b hb hab
rw [← h ha, ← h hb]
exact h₁ ha hb hab
