monotoneOn_or_antitoneOn — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem monotoneOn_or_antitoneOn [LinearOrder β] (hf : QuasilinearOn 𝕜 s f) : MonotoneOn f s ∨ AntitoneOn f s :=
  by
  simp_rw [monotoneOn_or_antitoneOn_iff_uIcc, ← segment_eq_uIcc]
  rintro a ha b hb c _ h
  refine ⟨((hf.2 _).segment_subset ?_ ?_ h).2, ((hf.1 _).segment_subset ?_ ?_ h).2⟩ <;> simp [*]

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