Mathlib Map

Theorems · Definition · order theory

SetRel.preimage

{α : Type u_1} → {β : Type u_2} → SetRel α β → Set β → Set α

Preimage of a set t under a relation R. Same as the image of t under R.inv.

Defined in
Mathlib.Data.Rel
Cited by
56 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

hausdorffEntourage · cited by 35hausdorffEntourageFilter.TotallyBounded · cited by 24Filter.TotallyBoundedPFun.preimage · cited by 18PFun.preimageSetRel.preimage_subset_preimage · cited by 7SetRel.preimage_subset_pr…Filter.TotallyBounded.mono · cited by 6TotallyBounded.monoSetRel.preimage_comp · cited by 5SetRel.preimage_compSetRel.preimage_subset_preimage_left · cited by 5SetRel.preimage_subset_pr…SetRel.preimage_mono · cited by 4SetRel.preimage_monoUltrafilter.cauchy_of_totallyBounded' · cited by 4Ultrafilter.cauchy_of_tot…Filter.rcomap' · cited by 4Filter.rcomap'UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen · cited by 4hausdorff.isOpen_inter_no…UniformSpace.closure_subset_preimage · cited by 3UniformSpace.closure_subs…mem_hausdorffEntourage · cited by 3mem_hausdorffEntourageFilter.TotallyBounded.totallyBounded_setOfPred_clusterPt · cited by 3TotallyBounded.totallyBou…SetRel.preimage_eq_biUnion · cited by 2SetRel.preimage_eq_biUnionSet · cited by 53352SetSet.ofPred · cited by 6101Set.ofPredSetRel · cited by 581SetRelSetRel.preimageCITED BYCITES

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
  • Set.ofPredproof · cited by 6,101
  • SetRelstatement and proof · cited by 581

Cited by60

Results whose statement or proof uses this declaration.