Theorems · Theorem · general topology
Metric.eball_mem_nhds
∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) {ε : ENNReal}, 0 < ε → Metric.eball x ε ∈ nhds x- Defined in
- Mathlib.Topology.EMetricSpace.Defs
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 145 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PseudoEMetricSpace
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 · cited by 53,352
- ENNRealstatement and proof · cited by 9,879
- Filterstatement · cited by 8,121
- nhdsstatement · cited by 5,554
- PseudoEMetricSpacestatement and proof · cited by 1,536
- IsOpen.mem_nhdsproof · cited by 470
- Metric.eballstatement · cited by 294
- Metric.isOpen_eballproof · cited by 13
- Metric.mem_eball_selfproof · cited by 6
Cited by25
Results whose statement or proof uses this declaration.
- isOpen_analyticAtproof · cited by 6
- HasFPowerSeriesAt.continuousAtproof · cited by 6
- Metric.closedEBall_mem_nhdsproof · cited by 4
- continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWithproof · cited by 3
- isOpen_cpolynomialAtproof · cited by 3
- hasFDerivAt_exp_smul_const_of_mem_ballproof · cited by 3
- HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_subproof · cited by 2
- HasFPowerSeriesOnBall.eventually_hasSum_subproof · cited by 2
- ContinuousWithinAt.oscillationWithin_eq_zeroproof · cited by 2
- HasFPowerSeriesWithinOnBall.continuousWithinAt_insertproof · cited by 2
- HasFPowerSeriesWithinAt.compproof · cited by 2
- AnalyticAt.eventually_continuousAtproof · cited by 1