strictAnti_iff_Icc — Mathlib

English

For AddConstMapClass with ha > 0, f is StrictMono iff it is StrictMonoOn on the interval Icc(l, l+a).

Русский

При ha > 0 функция f строгомонотонна тогда и только тогда, когда она строгомонотонна на интервале Icc(l, l+a).

LaTeX

$$$\text{StrictMono}(f) \iff \text{StrictMonoOn}(f, Icc(l, l+a)).$$$

Lean4

theorem strictAnti_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) :
    StrictAnti f ↔ StrictAntiOn f (Icc l (l + a)) :=
  strictMono_iff_Icc (H := Hᵒᵈ) ha l

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