Theorems · Theorem · general topology
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} (f : β → α),
Filter.Tendsto f l (nhds a) → (∀ᶠ (x : β) in l, f x ∈ s) → Filter.Tendsto f l (nhdsWithin a s)- Defined in
- Mathlib.Topology.NhdsWithin
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 52 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement and proof · cited by 8,121
- nhdsstatement and proof · cited by 5,554
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.Eventuallystatement and proof · cited by 3,134
- nhdsWithinstatement · cited by 1,912
- Filter.tendsto_principalproof · cited by 28
- Filter.tendsto_infproof · cited by 23
Cited by28
Results whose statement or proof uses this declaration.
- tendsto_nhdsWithin_iffproof · cited by 37
- StieltjesFunction.measure_singletonproof · cited by 6
- HasDerivAt.lhopital_zero_right_on_Iooproof · cited by 5
- tendsto_riemannZeta_sub_one_divproof · cited by 3
- Function.Periodic.qParam_tendstoproof · cited by 3
- MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_leproof · cited by 2
- Monotone.tendsto_leftLim_withinproof · cited by 2
- Complex.nhdsWithin_lt_le_nhdsWithin_stolzSetproof · cited by 1
- MeasureTheory.measure_le_measure_closure_of_levyProkhorovEDist_eq_zeroproof · cited by 1
- BoundedVariationOn.vectorMeasure_singletonproof · cited by 1
- Real.tendsto_cos_neg_pi_div_twoproof · cited by 1
- Real.tendsto_cos_pi_div_twoproof · cited by 1