Theorems · Definition · general topology
hausdorffEntourage
{α : Type u_1} → SetRel α α → SetRel (Set α) (Set α)The set of pairs of sets contained in each other's thickening with respect to an entourage.
- Defined in
- Mathlib.Topology.UniformSpace.Closeds
- Cited by
- 35 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
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 and proof · cited by 53,352
- Set.ofPredproof · cited by 6,101
- SetRelstatement and proof · cited by 581
- SetRel.preimageproof · cited by 56
- SetRel.imageproof · cited by 49
Cited by36
Results whose statement or proof uses this declaration.
- UniformSpace.hausdorffproof · cited by 33
- Filter.HasBasis.uniformity_hausdorffstatement · cited by 8
- monotone_hausdorffEntouragestatement · cited by 5
- UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpenproof · cited by 4
- TotallyBounded.powerset_hausdorffproof · cited by 3
- IsUniformInducing.image_hausdorffproof · cited by 3
- mem_hausdorffEntouragestatement · cited by 3
- UniformSpace.hausdorff.uniformContinuous_prodproof · cited by 3
- UniformSpace.hausdorff.uniformContinuous_unionproof · cited by 3
- UniformSpace.hausdorff.isClopen_singleton_emptyproof · cited by 2
- UniformSpace.hausdorff.isClosed_setOfPred_totallyBoundedproof · cited by 2
- UniformSpace.hausdorff.isUniformInducing_closureproof · cited by 2