Theorems · Theorem · functional analysis
Metric.closedBall_infDist_compl_subset_closure
∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [NormedSpace ℝ F] {x : F} {s : Set F},
x ∈ s → Metric.closedBall x (Metric.infDist x sᶜ) ⊆ closure s- Cited by
- 1 results in Mathlib
- Foundations
- Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
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
- Realstatement and proof · cited by 25,697
- NormedSpacestatement and proof · cited by 12,499
- Compl.complstatement and proof · cited by 2,925
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- closurestatement and proof · cited by 1,254
- eq_or_neproof · cited by 1,117
- Metric.closedBallstatement and proof · cited by 704
- Set.singleton_subset_iffproof · cited by 206
- closure_monoproof · cited by 133
- Metric.infDiststatement and proof · cited by 68
- closure_ballproof · cited by 20
Cited by1
Results whose statement or proof uses this declaration.
- exists_mem_frontier_infDist_compl_eq_distproof · cited by 2