case intro
y : ℝ*
r s : ℝ
hys : IsSt y s
hrs : r < s
f : ℕ → ℝ
hxr : IsSt (ofSeq f) r
⊢ ofSeq f < y
x y : ℝ*
r s : ℝ
hxr : IsSt x r
hys : IsSt y s
hrs : r < s
⊢ x < y
rcases ofSeq_surjective x with ⟨f, rfl⟩
case intro.intro
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : IsSt (ofSeq f) r
g : ℕ → ℝ
hys : IsSt (ofSeq g) s
⊢ ofSeq f < ofSeq g
case intro
y : ℝ*
r s : ℝ
hys : IsSt y s
hrs : r < s
f : ℕ → ℝ
hxr : IsSt (ofSeq f) r
⊢ ofSeq f < y
rcases ofSeq_surjective y with ⟨g, rfl⟩
case intro.intro
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
g : ℕ → ℝ
hys : Tendsto g (↑(hyperfilter ℕ)) (𝓝 s)
⊢ ofSeq f < ofSeq g
case intro.intro
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : IsSt (ofSeq f) r
g : ℕ → ℝ
hys : IsSt (ofSeq g) s
⊢ ofSeq f < ofSeq g
rw [isSt_ofSeq_iff_tendsto] at hxr hys
no goals
case intro.intro
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
g : ℕ → ℝ
hys : Tendsto g (↑(hyperfilter ℕ)) (𝓝 s)
⊢ ofSeq f < ofSeq g
exact ofSeq_lt_ofSeq.2 <| hxr.eventually_lt hys hrs