English
For monotone f on Ioi or Iio with bounds, Tendsto to sInf/sSup of the image holds from the corresponding side.
Русский
Для монотонной f на Ioi или Iio с границами верно сходение к sInf/sSup образа слева или справа от точки.
LaTeX
$$$\mathrm{MonotoneOn}(f, Ioi(x)) \Rightarrow \mathrm{Tendsto}\, f\,(\mathcal{N}_{[>]}(x))\,(\mathcal{N}(\mathrm{sInf}(f'' Ioi(x))))$$$
Lean4
/-- If `f` is a function strictly monotone on a right neighborhood of `a` and the
image of this neighborhood under `f` meets every interval `(f a, b]`, `b > f a`, then `f` is
continuous at `a` from the right.
The assumption `hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b` is required because otherwise the
function `f : ℝ → ℝ` given by `f x = if x ≤ 0 then x else x + 1` would be a counter-example at
`a = 0`. -/
theorem continuousWithinAt_right_of_exists_between {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s)
(hs : s ∈ 𝓝[≥] a) (hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b) : ContinuousWithinAt f (Ici a) a :=
by
have ha : a ∈ Ici a := left_mem_Ici
have has : a ∈ s := mem_of_mem_nhdsWithin ha hs
refine tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩
·
filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using
hb.trans_le ((h_mono.le_iff_le has hxs).2 hxa)
· rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
rw [h_mono.lt_iff_lt has hcs] at hac
filter_upwards [hs, Ico_mem_nhdsGE hac]
rintro x hx ⟨_, hxc⟩
exact ((h_mono.lt_iff_lt hx hcs).2 hxc).trans_le hcb
