English
If f is monotone on s, x is a cluster point of s and f is continuous within s at x, then f is monotone on insert x s.
Русский
Если f монотонна на s, x — кластерная точка s, и f непрерывна внутри s в точке x, то f монотонна на вставке x в s.
LaTeX
$$$MonotoneOn\ f\ s \rightarrow ClusterPt\ x\ (Filter.principal\ s) \rightarrow ContinuousWithinAt\ f\ s\ x \rightarrow MonotoneOn\ f\ (\text{insert } x\ s)$$$
Lean4
theorem insert_of_continuousWithinAt [TopologicalSpace β] [OrderClosedTopology β] (hf : MonotoneOn f s)
(hx : ClusterPt x (𝓟 s)) (h'x : ContinuousWithinAt f s x) : MonotoneOn f (insert x s) :=
by
have : (𝓝[s] x).NeBot := hx
apply monotoneOn_insert_iff.2 ⟨fun b hb hbx ↦ ?_, fun b hb hxb ↦ ?_, hf⟩
· rcases hbx.eq_or_lt with rfl | hbx
· exact le_rfl
simp only [ContinuousWithinAt] at h'x
apply ge_of_tendsto h'x
have : s ∩ Ioi b ∈ 𝓝[s] x := inter_mem_nhdsWithin _ (Ioi_mem_nhds hbx)
filter_upwards [this] with y hy using hf hb hy.1 (le_of_lt hy.2)
· rcases hxb.eq_or_lt with rfl | hxb
· exact le_rfl
simp only [ContinuousWithinAt] at h'x
apply le_of_tendsto h'x
have : s ∩ Iio b ∈ 𝓝[s] x := inter_mem_nhdsWithin _ (Iio_mem_nhds hxb)
filter_upwards [this] with y hy
exact hf hy.1 hb (le_of_lt hy.2)
