Theorems · Theorem · general topology
UniformSpace.mem_ball_symmetry
∀ {β : Type ub} {V : SetRel β β} [V.IsSymm] {x y : β}, x ∈ UniformSpace.ball y V ↔ y ∈ UniformSpace.ball x V- Defined in
- Mathlib.Topology.UniformSpace.Defs
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- SetRel.IsSymm
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- SetRelstatement and proof · cited by 581
- UniformSpace.ballstatement · cited by 113
- SetRel.IsSymmstatement and proof · cited by 93
- SetRel.commproof · cited by 5
Cited by9
Results whose statement or proof uses this declaration.
- UniformSpace.subset_countable_closure_of_almost_dense_setproof · cited by 4
- UniformSpace.mem_comp_of_mem_ballproof · cited by 4
- Disjoint.exists_uniform_thickeningproof · cited by 1
- UniformSpace.ball_eq_of_symmetryproof · cited by 1
- Dynamics.mem_ball_dynEntourage_compproof · cited by 1
- EquicontinuousAt.tendsto_of_mem_closureproof · cited by 1
- UniformSpace.mem_comp_compproof · cited by 0
- closure_image_mem_nhds_of_isUniformInducingproof · cited by 0
- ball_eq_of_memproof · cited by 0