English
For M > 1, the image of nhdsWithin around 1 under ofReal is contained in nhdsWithin around 1 for stolzSet M; i.e., the Stolz set captures a neighborhood boundary.
Русский
Для M > 1 образ nhdsWithin вокруг 1 под действием ofReal лежит внутри nhdsWithin вокруг 1 для stolzSet M; т. е. множество Стольца задаёт границу окрестности.
LaTeX
$$$(\\mathcal{N}_[<]\,1).map(\\operatorname{ofReal}) \\le \\mathcal{N}_{[stolzSet M]} 1$$$
Lean4
theorem nhdsWithin_lt_le_nhdsWithin_stolzSet {M : ℝ} (hM : 1 < M) : (𝓝[<] 1).map ofReal ≤ 𝓝[stolzSet M] 1 :=
by
rw [← tendsto_id']
refine
tendsto_map' <|
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within ofReal
(tendsto_nhdsWithin_of_tendsto_nhds <| ofRealCLM.continuous.tendsto' 1 1 rfl) ?_
simp only [eventually_iff, mem_nhdsWithin]
refine ⟨Set.Ioo 0 2, isOpen_Ioo, by simp, fun x hx ↦ ?_⟩
simp only [Set.mem_inter_iff, Set.mem_Ioo, Set.mem_Iio] at hx
simp only [Set.mem_setOf_eq, stolzSet, ← ofReal_one, ← ofReal_sub, norm_real, norm_of_nonneg hx.1.1.le,
norm_of_nonneg <| (sub_pos.mpr hx.2).le]
exact
⟨hx.2, lt_mul_left (sub_pos.mpr hx.2) hM⟩
-- An ugly technical lemma
