case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
obtain ⟨x, x_pos, hx⟩ := stirlingSeq'_bounded_by_pos_constant
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
have hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ)) := by simpa [lowerBounds] using hx
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto stirlingSeq atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
refine' ⟨_, lt_of_lt_of_le x_pos (le_csInf (Set.range_nonempty _) hx'), _⟩
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto (fun n => stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto stirlingSeq atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
rw [← Filter.tendsto_add_atTop_iff_nat 1]
no goals
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto (fun n => stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
exact tendsto_atTop_ciInf stirlingSeq'_antitone ⟨x, hx'⟩
no goals
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
⊢ x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
simpa [lowerBounds] using hx