trans_monovary — Mathlib

English

If f is strictly antitone and g monovaries with f, then g is antitone.

Русский

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

LaTeX

$$$$ (StrictAnti\\;f) \\land (Monovary\\;g\\;f) \\Rightarrow Antitone\\;g $$$$

Lean4

theorem trans_monovary (hf : StrictAnti f) (h : Monovary g f) : Antitone g :=
  antitone_iff_forall_lt.2 fun _a _b hab ↦ h <| hf hab

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