Theorems · Theorem · general topology
Metric.closure_ball_subset_closedBall
∀ {α : Type u_2} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, closure (Metric.ball x ε) ⊆ Metric.closedBall x ε- Cited by
- 10 results in Mathlib
- Foundations
- Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PseudoMetricSpace
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
- Realstatement and proof · cited by 25,697
- PseudoMetricSpacestatement and proof · cited by 1,550
- closurestatement · cited by 1,254
- Metric.ballstatement · cited by 735
- Metric.closedBallstatement · cited by 704
- closure_minimalproof · cited by 94
- Metric.ball_subset_closedBallproof · cited by 46
- Metric.isClosed_closedBallproof · cited by 28
Cited by10
Results whose statement or proof uses this declaration.
- closure_ballproof · cited by 20
- DifferentiableOn.hasFPowerSeriesOnBallproof · cited by 4
- DifferentiableOn.circleIntegral_one_div_sub_center_pow_smulproof · cited by 2
- Complex.norm_eventually_eq_of_isLocalMaxproof · cited by 2
- circleAverage_re_herglotzRieszKernel_mul_log₀proof · cited by 1
- DiffContOnCl.mk_ballproof · cited by 1
- Complex.eventually_eq_of_isLocalMax_normproof · cited by 1
- MeasureTheory.isTightMeasureSet_of_isCompact_closureproof · cited by 0
- DifferentiableOn.circleIntegral_sub_inv_smulproof · cited by 0
- InnerProductSpace.HarmonicContOnCl.mk_ballproof · cited by 0