Theorems · Theorem · order theory
Set.BijOn.image_eq
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.BijOn f s t → f '' s = t- Defined in
- Mathlib.Data.Set.Function
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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.imagestatement · cited by 5,609
- Set.BijOnstatement and proof · cited by 168
- Set.BijOn.mapsToproof · cited by 42
- Set.BijOn.surjOnproof · cited by 31
- Set.SurjOn.image_eq_of_mapsToproof · cited by 3
Cited by30
Results whose statement or proof uses this declaration.
- PartialEquiv.image_source_eq_targetproof · cited by 18
- Matroid.map_isBase_iffproof · cited by 5
- Set.image_add_const_Iccproof · cited by 3
- Set.image_add_const_Icoproof · cited by 3
- Set.image_add_const_Iocproof · cited by 3
- Set.image_add_const_Iooproof · cited by 3
- Module.eq_of_mapsTo_reflection_of_memproof · cited by 2
- Set.BijOn.exists_extend_of_subsetproof · cited by 2
- Set.BijOn.iInf_compproof · cited by 2
- Set.BijOn.iSup_compproof · cited by 2
- IsMulFreimanIso.threeGPFree_congrproof · cited by 1
- Function.Semiconj.bijOn_imageproof · cited by 1