trans_antivaryOn — Mathlib

English

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

Русский

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

LaTeX

$$$$ (StrictMonoOn\\;f\\;s) \\land (AntivaryOn\\;g\\;f\\;s) \\Rightarrow AntitoneOn\\;g\\;s $$$$

Lean4

theorem trans_antivaryOn (hf : StrictMonoOn f s) (h : AntivaryOn g f s) : AntitoneOn g s :=
  antitoneOn_iff_forall_lt.2 fun _a ha _b hb hab ↦ h ha hb <| hf ha hb hab

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