trans_monovaryOn — Mathlib

English

If f is strictly monotone on a set and g monovaries with f on that set, then g is monotone on the set.

Русский

Если f строго монотонна на области и g моновариантна по отношению к f на этой области, то g монотонна на этой области.

LaTeX

$$$$ (StrictMonoOn\\;f\\;s) \\land (MonovaryOn\\;g\\;f\\;s) \\Rightarrow MonotoneOn\\;g\\;s $$$$

Lean4

theorem trans_monovaryOn (hf : StrictMonoOn f s) (h : MonovaryOn g f s) : MonotoneOn g s :=
  monotoneOn_iff_forall_lt.2 fun _a ha _b hb hab ↦ h ha hb <| hf ha hb hab

Похожие утверждения