LeanPool.VirasoroProject.ToMathlib.Topology.Order

theorem DiscreteTopology.tendsto_nhds_iff_eventually_eq {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] {ι : Type u_2} {F : Filter ι} (f : ι → X) (x : X) : Filter.Tendsto f F (nhds x) ↔ ∀ᶠ (i : ι) in F, f i = x