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 : StrictAntiOn f s) (h : MonovaryOn g f s) : AntitoneOn g s :=
  antitoneOn_iff_forall_lt.2 fun _a ha _b hb hab ↦ h hb ha <| hf ha hb hab

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