Theorems · Theorem · order theory
Set.MapsTo.image_subset
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.MapsTo f s t → f '' s ⊆ t- Defined in
- Mathlib.Data.Set.Function
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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.MapsTostatement and proof · cited by 732
- Set.mapsTo_iff_image_subsetproof · cited by 18
Cited by49
Results whose statement or proof uses this declaration.
- image_closure_subset_closure_imageproof · cited by 21
- IsOpenMap.image_interior_subsetproof · cited by 6
- TendstoLocallyUniformlyOn.compproof · cited by 5
- Set.SurjOn.image_eq_of_mapsToproof · cited by 3
- Set.image_iInter_subsetproof · cited by 3
- Set.image_iInter₂_subsetproof · cited by 3
- IsOpenMap.mapsTo_interiorproof · cited by 3
- smul_closure_subsetproof · cited by 3
- StrictAntiOn.image_Ico_subsetproof · cited by 2
- StrictAntiOn.image_Iio_subsetproof · cited by 2
- StrictAntiOn.image_Ioc_subsetproof · cited by 2
- StrictAntiOn.image_Ioi_subsetproof · cited by 2