Theorems · Theorem · general topology
Metric.mem_closure_iff
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {a : α}, a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < εε-characterization of the closure in pseudometric spaces
- Defined in
- Mathlib.Topology.MetricSpace.Pseudo.Defs
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 115 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.
Cites8
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
- PseudoMetricSpacestatement and proof · cited by 1,550
- Dist.diststatement and proof · cited by 1,539
- closurestatement · cited by 1,254
- dist_commproof · cited by 188
- Metric.nhds_basis_ballproof · cited by 41
- mem_closure_iff_nhds_basisproof · cited by 13
Cited by18
Results whose statement or proof uses this declaration.
- Metric.closedBall_zero'proof · cited by 4
- ContinuousMap.idealOfSet_ofIdeal_eq_closureproof · cited by 2
- SeminormedAddCommGroup.mem_closure_iffproof · cited by 2
- IsUpperSet.exists_subset_ballproof · cited by 2
- IsLowerSet.exists_subset_ballproof · cited by 2
- MeasureTheory.ae_eq_zero_of_forall_dual_of_isSeparableproof · cited by 2
- ContinuousLinearMap.exists_approx_preimage_norm_leproof · cited by 1
- IsLowerSet.mem_interior_of_forall_ltproof · cited by 1
- Metric.mem_of_closed'proof · cited by 1
- Submodule.starProjection_tendsto_closure_iSupproof · cited by 1
- cauchy_map_of_uniformCauchySeqOn_fderivproof · cited by 1
- LipschitzWith.hasFDerivAt_of_hasLineDerivAt_of_closureproof · cited by 1