Theorems · Theorem · general topology
eventually_mem_nhdsWithin
∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, ∀ᶠ (x : α) in nhdsWithin a s, x ∈ s- Defined in
- Mathlib.Topology.NhdsWithin
- Cited by
- 35 results in Mathlib
- Foundations
- Depth 50 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Filter.Eventuallystatement · cited by 3,134
- nhdsWithinstatement · cited by 1,912
- self_mem_nhdsWithinproof · cited by 215
Cited by35
Results whose statement or proof uses this declaration.
- exists_fun_of_mem_tangentConeAtproof · cited by 9
- Filter.EventuallyEq.fderivWithin'proof · cited by 5
- EquicontinuousWithinAt.closure'proof · cited by 3
- tendsto_log_mul_rpow_nhdsGT_zeroproof · cited by 3
- disjoint_interior_extremePointsproof · cited by 2
- comap_coe_nhdsLT_eq_atTop_iffproof · cited by 2
- meromorphicOrderAt_deriv_eq_sub_oneproof · cited by 2
- not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioiproof · cited by 2
- UniformContinuousOn.comp_tendstoLocallyUniformlyOnproof · cited by 2
- HasFDerivWithinAt.eventually_neproof · cited by 2
- iteratedFDerivWithin_compproof · cited by 2