trans_antivaryOn — Mathlib

English

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

Русский

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

LaTeX

$$$$ (StrictAntiOn\\;f\\;s) \\land (AntivaryOn\\;g\\;f\\;s) \\Rightarrow MonotoneOn\\;g\\;s $$$$

Lean4

theorem trans_antivaryOn (hf : StrictAntiOn f s) (h : AntivaryOn g f s) : MonotoneOn g s :=
  monotoneOn_iff_forall_lt.2 fun _a ha _b hb hab ↦ h hb ha <| hf ha hb hab

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