Theorems · Definition · logic and foundations
Set.SurjOn
{α : Type u} → {β : Type v} → (α → β) → Set α → Set β → Propf is surjective from s to t if t is contained in the image of s.
- Defined in
- Mathlib.Data.Set.Operations
- Cited by
- 186 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 16 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by188
Results whose statement or proof uses this declaration.
- Set.BijOnproof · cited by 168
- Set.BijOn.surjOnstatement · cited by 31
- Set.surjOn_imagestatement · cited by 15
- Set.SurjOn.monostatement and proof · cited by 13
- Finset.sum_nbijstatement and proof · cited by 10
- Set.SurjOn.rightInvOn_invFunOnstatement and proof · cited by 9
- Finset.sum_of_injOnproof · cited by 8
- Set.SurjOn.mapsTo_invFunOnstatement and proof · cited by 7
- Set.SurjOn.subset_rangestatement and proof · cited by 6
- PartialEquiv.surjOnstatement · cited by 6
- Set.BijOn.mkstatement and proof · cited by 5
- isComplete_image_iffproof · cited by 5