Theorems · Theorem · general topology
UniformSpace.ball_mono
∀ {β : Type ub} {V W : Set (β × β)}, V ⊆ W → ∀ (x : β), UniformSpace.ball x V ⊆ UniformSpace.ball x W- Defined in
- Mathlib.Topology.UniformSpace.Defs
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- UniformSpace.ballstatement · cited by 113
- Set.preimage_monoproof · cited by 95
Cited by20
Results whose statement or proof uses this declaration.
- UniformSpace.subset_countable_closure_of_almost_dense_setproof · cited by 4
- Filter.HasBasis.lebesgue_number_lemmaproof · cited by 3
- EMetric.subset_countable_closure_of_almost_dense_setproof · cited by 2
- TopologicalSpace.IsSeparable.exists_countable_dense_subsetproof · cited by 2
- Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAtproof · cited by 2
- Dynamics.coverMincard_le_netMaxcardproof · cited by 2
- UniformSpace.ball_inter_leftproof · cited by 2
- UniformSpace.ball_inter_rightproof · cited by 2
- Dynamics.IsDynNetIn.of_entourage_subsetproof · cited by 1
- Dynamics.IsDynNetIn.of_leproof · cited by 1
- Disjoint.exists_uniform_thickening_of_basisproof · cited by 1
- Filter.HasBasis.lebesgue_number_lemma_nhdsproof · cited by 1