English
If f is monotone on s, a is the LUB of s, and f tends to b along nhds within a, then b is an upper bound of f(s).
Русский
Если f монотонно на s, a является наим. верхней границей s, и f стремится к b по nhds внутри a, тогда b является верхней границей множества f(s).
LaTeX
$$MonotoneOn f s → IsLUB s a → Tendsto f (nhdsWithin a s) (nhds b) → b ∈ upperBounds (f '' s)$$
Lean4
theorem mem_upperBounds_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α}
{a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : b ∈ upperBounds (f '' s) :=
by
rintro _ ⟨x, hx, rfl⟩
replace ha := ha.inter_Ici_of_mem hx
haveI := ha.nhdsWithin_neBot ⟨x, hx, le_rfl⟩
refine ge_of_tendsto (hb.mono_left (nhdsWithin_mono a (inter_subset_left (t := Ici x)))) ?_
exact
mem_of_superset self_mem_nhdsWithin fun y hy =>
hf hx hy.1
hy.2
-- For a version of this theorem in which the convergence considered on the domain `α` is as `x : α`
-- tends to infinity, rather than tending to a point `x` in `α`, see `isLUB_of_tendsto_atTop`
