Theorems · Theorem · general topology
refl_mem_uniformity
∀ {α : Type ua} [inst : UniformSpace α] {x : α} {s : SetRel α α}, s ∈ uniformity α → (x, x) ∈ s- Defined in
- Mathlib.Topology.UniformSpace.Defs
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- UniformSpace
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.
- Filterstatement · cited by 8,121
- UniformSpacestatement and proof · cited by 2,040
- uniformitystatement and proof · cited by 765
- SetRelstatement and proof · cited by 581
- refl_le_uniformityproof · cited by 4
Cited by15
Results whose statement or proof uses this declaration.
- isRefl_of_mem_uniformityproof · cited by 6
- UniformSpace.mem_ball_selfproof · cited by 3
- Set.Finite.totallyBoundedproof · cited by 3
- continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAtproof · cited by 2
- tendsto_diag_uniformityproof · cited by 2
- nhdsSet_diagonal_eq_uniformityproof · cited by 2
- IsSeqCompact.isCompleteproof · cited by 1
- TotallyBounded.nhds_vietoris_le_nhds_hausdorffproof · cited by 1
- TendstoUniformlyOn.lowerHemicontinuousOnproof · cited by 1
- CauchySeq.totallyBounded_rangeproof · cited by 1
- completeSpace_extensionproof · cited by 0
- t0Space_iff_ker_uniformityproof · cited by 0