bddAbove_slope_gt_of_mem_interior

English

A technical matching variant of HasDerivWithinAt_sInf_slope establishing the derivative via the infimum of slopes over a subset.

Русский

Техническая версия HasDerivWithinAt_sInf_slope через инфиминум наклонов на подмножествах.

LaTeX

$$$\\forall {S} {f} {x},\\; \\text{ConvexOn } \\mathbb{R} \\; S \\; f \\Rightarrow \\text{HasDerivWithinAt f \\; (\\sInf (\\text{image } (\\text{slope } f x) (\\{y\\in S \\mid x

Lean4

theorem bddAbove_slope_gt_of_mem_interior (hfc : ConvexOn 𝕜 s f) (hxs : x ∈ interior s) :
    BddAbove (slope f x '' {y ∈ s | y < x}) :=
  by
  obtain ⟨y, hyx, hys⟩ : ∃ y, x < y ∧ y ∈ s := Eventually.exists_gt (mem_interior_iff_mem_nhds.mp hxs)
  refine bddAbove_iff_subset_Iic.mpr ⟨slope f x y, fun y' ⟨z, hz, hz'⟩ ↦ ?_⟩
  simp_rw [mem_Iic, ← hz']
  refine hfc.slope_mono (interior_subset hxs) ?_ ?_ (hz.2.trans hyx).le
  · simp [hz.2.ne, hz.1]
  · simp [hys, hyx.ne']

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