Mathlib Map

Theorems · Theorem · order theory

Set.BijOn.mk

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
  Set.MapsTo f s t → Set.InjOn f s → Set.SurjOn f s t → Set.BijOn f s t
Defined in
Mathlib.Data.Set.Function
Cited by
5 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.InjOn.bijOn_image · cited by 20InjOn.bijOn_imageSet.BijOn.comp · cited by 6BijOn.compSet.BijOn.congr · cited by 3BijOn.congrNumberField.finite_setOfPred_prod_infinitePlace_iSup_le · cited by 2NumberField.finite_setOfP…SimpleGraph.ConnectedComponent.Represents.image_out · cited by 0Represents.image_outSet · cited by 53352SetSet.MapsTo · cited by 732Set.MapsToSet.InjOn · cited by 543Set.InjOnSet.SurjOn · cited by 186Set.SurjOnSet.BijOn · cited by 168Set.BijOnBijOn.mkCITED BYCITES

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.MapsTostatement and proof · cited by 732
  • Set.InjOnstatement and proof · cited by 543
  • Set.SurjOnstatement and proof · cited by 186
  • Set.BijOnstatement · cited by 168

Cited by5

Results whose statement or proof uses this declaration.