tendsto_nhdsLT — Mathlib

English

Let f be monotone on Ioi x with image bounded below; then f tends to the infimum of f''Ioi x from the right of x.

Русский

Пусть f монотонна на Ioi x и образ f''Ioi x ограничен снизу; тогда f стремится к наибольшему нижнему пределу образов справа от x.

LaTeX

$$$\text{MonotoneOn}(f, Ioi(x)) \wedge \text{BddBelow}(f'' Ioi(x)) \Rightarrow \mathrm{Tendsto}\, f\,(\mathcal{N}_{[>]}(x))\,(\mathcal{N}(\inf (f'' Ioi(x))))$$$

Lean4

theorem tendsto_nhdsLT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
    [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α}
    (Mf : MonotoneOn f (Iio x)) (h_bdd : BddAbove (f '' Iio x)) : Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x))) :=
  by
  rcases eq_empty_or_nonempty (Iio x) with (h | h); · simp [h]
  refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
  · obtain ⟨z, zx, lz⟩ : ∃ a : α, a < x ∧ l < f a := by
      simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using exists_lt_of_lt_csSup (h.image _) hl
    filter_upwards [Ioo_mem_nhdsLT zx] with y hy using lz.trans_le (Mf zx hy.2 hy.1.le)
  · refine mem_of_superset self_mem_nhdsWithin fun y hy => lt_of_le_of_lt ?_ hm
    exact le_csSup h_bdd (mem_image_of_mem _ hy)

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