Theorems · Theorem · general topology
Metric.hasBasis_cobounded_compl_closedBall
∀ {α : Type u} [inst : PseudoMetricSpace α] (c : α),
(Bornology.cobounded α).HasBasis (fun x => True) fun r => (Metric.closedBall c r)ᶜ- Defined in
- Mathlib.Topology.MetricSpace.Bounded
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 105 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.
Cites10
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
- Compl.complstatement · cited by 2,925
- PseudoMetricSpacestatement and proof · cited by 1,550
- Metric.closedBallstatement and proof · cited by 704
- Filter.HasBasisstatement · cited by 604
- Function.Surjective.forallproof · cited by 214
- Bornology.coboundedstatement · cited by 162
- compl_surjectiveproof · cited by 26
- Metric.isBounded_iff_subset_closedBallproof · cited by 10
Cited by3
Results whose statement or proof uses this declaration.
- Metric.cobounded_eq_cocompactproof · cited by 8
- Metric.hasAntitoneBasis_cobounded_compl_closedBallproof · cited by 1
- tendsto_integral_comp_smul_smul_of_integrableproof · cited by 1