Mathlib Map

Theorems · Theorem · order theory

Set.BijOn.mapsTo

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.BijOn f s t → Set.MapsTo f s t
Defined in
Mathlib.Data.Set.Function
Cited by
42 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.BijOn.image_eq · cited by 30BijOn.image_eqSet.Finite.of_finite_image · cited by 20Finite.of_finite_imageSet.BijOn.comp · cited by 6BijOn.compSet.BijOn.symm · cited by 6BijOn.symmSet.BijOn.equiv · cited by 5BijOn.equivSet.BijOn.inter_mapsTo · cited by 5BijOn.inter_mapsToSet.BijOn.toPartialEquiv · cited by 5BijOn.toPartialEquivIsAddFreimanIso.isAddFreimanHom · cited by 5IsAddFreimanIso.isAddFrei…Set.BijOn.congr · cited by 3BijOn.congrSet.BijOn.forall · cited by 3BijOn.forallEquiv.Perm.IsCycleOn.apply_mem_iff · cited by 3IsCycleOn.apply_mem_iffIsMulFreimanIso.isMulFreimanHom · cited by 3IsMulFreimanIso.isMulFrei…Set.BijOn.exists_extend_of_subset · cited by 2BijOn.exists_extend_of_su…Set.BijOn.bijective · cited by 2BijOn.bijectiveIsAddFreimanHom.addRothNumber_mono · cited by 2IsAddFreimanHom.addRothNu…Set · cited by 53352SetSet.MapsTo · cited by 732Set.MapsToSet.BijOn · cited by 168Set.BijOnBijOn.mapsToCITED 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.MapsTostatement · cited by 732
  • Set.BijOnstatement and proof · cited by 168

Cited by44

Results whose statement or proof uses this declaration.