nhdsWithin_stolzCone_le_nhdsWithin_stolzSet

English

For every s > 0, there exists M > 0 such that the neighborhood of 1 within the Stolz cone with parameter s is contained in the neighborhood of 1 within the Stolz set with parameter M.

Русский

Пусть s > 0. Существaет M > 0 такое, что окрестность числа 1 внутри конуса Стольца со параметром s содержится в окрестности 1 внутри множества Стольца с параметром M.

LaTeX

$$$$\\exists M>0,\, \\mathcal{N}_{\\operatorname{stolzCone}(s)}(1) \\\\le \\\\mathcal{N}_{\\operatorname{stolzSet}(M)}(1).$$$$

Lean4

theorem nhdsWithin_stolzCone_le_nhdsWithin_stolzSet {s : ℝ} (hs : 0 < s) : ∃ M, 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1 :=
  by
  obtain ⟨M, ε, _, hε, H⟩ := stolzCone_subset_stolzSet_aux hs
  use M
  rw [nhdsWithin_le_iff, mem_nhdsWithin]
  refine ⟨{w | 1 - ε < w.re}, isOpen_lt continuous_const continuous_re, ?_, H⟩
  simp only [Set.mem_setOf_eq, one_re, sub_lt_self_iff, hε]

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