antitone_iff_Icc — Mathlib

English

Similarly, f is antitone iff it is antitone on the interval Icc(l, l+a) for any l, under AddConstMapClass assumptions.

Русский

Аналогично: f антимонотонна тогда и только тогда, когда она антимонотонна на интервале Icc(l, l+a).

LaTeX

$$$\text{Antitone}(f) \iff \text{AntitoneOn}(f, Icc(l, l+a)).$$$

Lean4

theorem antitone_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [AddCommGroup H]
    [PartialOrder H] [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :
    Antitone f ↔ AntitoneOn f (Icc l (l + a)) :=
  monotone_iff_Icc (H := Hᵒᵈ) ha l

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