Mathlib Map

Theorems · Theorem · logic and foundations

Hyperreal.isSt_ofSeq_iff_tendsto

Deprecated since 2026-01-05Use Hyperreal.tendsto_iff_forall instead.

∀ {f : ℕ → ℝ} {r : ℝ}, (Hyperreal.ofSeq f).IsSt r ↔ Filter.Tendsto f (↑(Filter.hyperfilter ℕ)) (nhds r)
Defined in
Mathlib.Analysis.Real.Hyperreal
Cited by
7 results in Mathlib
Foundations
Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Hyperreal.isSt_refl_real · cited by 7Hyperreal.isSt_refl_realHyperreal.IsSt.unique · cited by 6IsSt.uniqueHyperreal.IsSt.map₂ · cited by 3IsSt.map₂Hyperreal.IsSt.lt · cited by 2IsSt.ltHyperreal.IsSt.map · cited by 2IsSt.mapHyperreal.isSt_of_tendsto · cited by 1Hyperreal.isSt_of_tendstoHyperreal.isSt_iff_tendsto · cited by 0Hyperreal.isSt_iff_tendstoReal · cited by 25697Realnhds · cited by 5554nhdsFilter.Tendsto · cited by 3814Filter.TendstoUltrafilter.toFilter · cited by 172Ultrafilter.toFilterFilter.HasBasis.tendsto_right_iff · cited by 81HasBasis.tendsto_right_iffHyperreal.IsSt · cited by 42Hyperreal.IsStIff.and · cited by 33Iff.andFilter.hyperfilter · cited by 30Filter.hyperfilterHyperreal.ofSeq · cited by 24Hyperreal.ofSeqHyperreal.ofSeq_lt_ofSeq · cited by 6Hyperreal.ofSeq_lt_ofSeqFilter.eventually_and · cited by 5Filter.eventually_andnhds_basis_Ioo_pos · cited by 4nhds_basis_Ioo_posHyperreal.isSt_ofSeq_iff_tend…CITED BYCITES

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by7

Results whose statement or proof uses this declaration.