strict_mono_of_lt — Mathlib

English

If f is convex on s and f x < f y for x < y in s, then f is strictly monotone on s ∩ [y, ∞).

Русский

Если f выпукла на s и f(x) < f(y) для x < y в s, то f строго возрастает на s ∩ [y, ∞).

LaTeX

$$$\text{ConvexOn } 𝕜\ s\ f \Rightarrow \forall x,y:\ x∈s, y∈s, x

Lean4

/-- If `f` is convex on a set `s` in a linearly ordered field, and `f x < f y` for two points
`x < y` in `s`, then `f` is strictly monotone on `s ∩ [y, ∞)`. -/
theorem strict_mono_of_lt (hf : ConvexOn 𝕜 s f) {x y : 𝕜} (hx : x ∈ s) (hxy : x < y) (hxy' : f x < f y) :
    StrictMonoOn f (s ∩ Set.Ici y) := by
  intro u hu v hv huv
  have step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z :=
    by
    intro z hz
    refine hf.lt_right_of_left_lt hx hz.1 ?_ hxy'
    rw [openSegment_eq_Ioo (hxy.trans hz.2)]
    exact ⟨hxy, hz.2⟩
  rcases eq_or_lt_of_le hu.2 with (rfl | hu2)
  · exact step1 ⟨hv.1, huv⟩
  · refine hf.lt_right_of_left_lt ?_ hv.1 ?_ (step1 ⟨hu.1, hu2⟩)
    · apply hf.1.segment_subset hx hu.1
      rw [segment_eq_Icc (hxy.le.trans hu.2)]
      exact ⟨hxy.le, hu.2⟩
    · rw [openSegment_eq_Ioo (hu2.trans huv)]
      exact ⟨hu2, huv⟩

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