Theorems · Theorem · general topology
IsUltraUniformity.hasBasis
∀ {X : Type u_1} {inst : UniformSpace X} [self : IsUltraUniformity X],
(uniformity X).HasBasis (fun s => s ∈ uniformity X ∧ s.IsSymm ∧ s.IsTrans) id- Cited by
- 5 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- IsUltraUniformity
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.
- Filterstatement · cited by 8,121
- UniformSpacestatement and proof · cited by 2,040
- uniformitystatement · cited by 765
- Filter.HasBasisstatement · cited by 604
- SetRelstatement · cited by 581
- SetRel.IsSymmstatement · cited by 93
- SetRel.IsTransstatement · cited by 21
- IsUltraUniformitystatement and proof · cited by 13
Cited by5
Results whose statement or proof uses this declaration.
- UniformSpace.nhds_basis_clopensproof · cited by 1
- IsUltraUniformity.comapproof · cited by 1
- IsUltraUniformity.iInfproof · cited by 0
- IsUltraUniformity.infproof · cited by 0
- IsUltraUniformity.mem_nhds_iff_symm_transproof · cited by 0