Theorems · Theorem · general topology
tendsto_atTop_of_eventually_const
∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {ι : Type u_2} [inst_1 : Preorder ι] {u : ι → X} {i₀ : ι},
(∀ i ≥ i₀, u i = x) → Filter.Tendsto u Filter.atTop (nhds x)- Defined in
- Mathlib.Topology.Neighborhoods
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpacePreorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Preorderstatement and proof · cited by 7,952
- nhdsstatement · cited by 5,554
- Filter.Tendstostatement · cited by 3,814
- Filter.atTopstatement · cited by 2,405
- Filter.Eventually.monoproof · cited by 646
- Filter.EventuallyEq.symmproof · cited by 408
- tendsto_const_nhdsproof · cited by 330
- Filter.Tendsto.congr'proof · cited by 154
- Filter.eventually_ge_atTopproof · cited by 111
Cited by14
Results whose statement or proof uses this declaration.
- Nat.Partition.hasProd_genFunproof · cited by 4
- IsTopologicallyNilpotent.zeroproof · cited by 1
- MvPowerSeries.WithPiTopology.tendsto_trunc'_atTopproof · cited by 1
- tendsto_smoothingFun_of_eq_zeroproof · cited by 1
- PowerSeries.WithPiTopology.tendsto_trunc_atTopproof · cited by 1
- cauchySeq_sum_of_eventually_eqproof · cited by 1
- MeasureTheory.tendsto_indicator_geproof · cited by 1
- MeasureTheory.Martingale.eq_condExp_of_tendsto_eLpNormproof · cited by 1
- thickenedIndicatorAux_tendsto_indicator_closureproof · cited by 1
- MvPowerSeries.WithPiTopology.tendsto_trunc_atTopproof · cited by 0
- tendsto_atBot_of_eventually_constproof · cited by 0