Theorems · Theorem · logic and foundations
Set.mapsTo_image
∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α), Set.MapsTo f s (f '' s)- Defined in
- Mathlib.Data.Set.Operations
- Cited by
- 71 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
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 · cited by 732
- Set.mem_image_of_memproof · cited by 371
Cited by71
Results whose statement or proof uses this declaration.
- image_closure_subset_closure_imageproof · cited by 21
- Set.InjOn.bijOn_imageproof · cited by 20
- IsOpenMap.image_interior_subsetproof · cited by 6
- isComplete_image_iffproof · cited by 5
- IsGreatest.nnnorm_cfc_nnrealproof · cited by 5
- IsGreatest.nnnorm_cfcₙ_nnrealproof · cited by 5
- mdifferentiableWithinAt_totalSpaceproof · cited by 5
- Bundle.contMDiffWithinAt_totalSpaceproof · cited by 5
- cfc_compproof · cited by 5
- ContinuousWithinAt.preimage_mem_nhdsWithin'proof · cited by 4
- intervalIntegral.integral_deriv_smul_comp'''proof · cited by 4
- Set.surjective_mapsTo_image_restrictstatement and proof · cited by 4