Theorems · Theorem · general topology
eventually_nhdsWithin_of_eventually_nhds
∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {a : α} {p : α → Prop},
(∀ᶠ (x : α) in nhds a, p x) → ∀ᶠ (x : α) in nhdsWithin a s, p x- Defined in
- Mathlib.Topology.NhdsWithin
- Cited by
- 17 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.
Cites6
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
- nhdsstatement and proof · cited by 5,554
- Filter.Eventuallystatement and proof · cited by 3,134
- nhdsWithinstatement · cited by 1,912
- mem_nhdsWithin_of_mem_nhdsproof · cited by 50
Cited by17
Results whose statement or proof uses this declaration.
- ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNEproof · cited by 6
- MeromorphicAt.derivproof · cited by 6
- toMeromorphicNFAt_eq_selfproof · cited by 4
- meromorphicNFAt_iff_analyticAt_orproof · cited by 3
- contMDiffWithinAt_finprodproof · cited by 2
- contMDiffWithinAt_finsumproof · cited by 2
- meromorphicOrderAt_ne_top_iff_eventually_ne_zeroproof · cited by 2
- AnalyticAt.preimage_of_nhdsNEproof · cited by 2
- Metric.exists_isCompact_closedBallproof · cited by 2
- OpenPartialHomeomorph.eventually_nhdsWithin'proof · cited by 1
- AnalyticOnNhd.codiscreteWithin_setOfPred_analyticOrderAt_eq_zero_or_topproof · cited by 1
- AnalyticOnNhd.codiscrete_setOfPred_analyticOrderAt_eq_zero_or_topproof · cited by 1