quasilinearOn_iff_monotoneOn_or_antitoneOn

English

For a convex set S, QuasilinearOn 𝕜 s f is equivalent to f being either monotone or antitone on s.

Русский

Для выпуклого множества S квазилинейность эквивалентна тому, что f либо монотонна, либо антонто́нна на S.

LaTeX

$$$QuasilinearOn\ 𝕜\ s\ f \iff MonotoneOn\ f\ s \lor AntitoneOn\ f\ s$$$

Lean4

theorem quasilinearOn_iff_monotoneOn_or_antitoneOn [LinearOrder β] (hs : Convex 𝕜 s) :
    QuasilinearOn 𝕜 s f ↔ MonotoneOn f s ∨ AntitoneOn f s :=
  ⟨fun h => h.monotoneOn_or_antitoneOn, fun h => h.elim (fun h => h.quasilinearOn hs) fun h => h.quasilinearOn hs⟩

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