Theorems · Theorem · order theory
Set.subset_preimage_image
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), s ⊆ f ⁻¹' f '' s- Defined in
- Mathlib.Data.Set.Image
- Cited by
- 44 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.preimagestatement · cited by 4,946
- Set.mem_image_of_memproof · cited by 371
Cited by44
Results whose statement or proof uses this declaration.
- Set.preimage_image_eqproof · cited by 87
- Filter.image_mem_mapproof · cited by 39
- ContinuousOn.aestronglyMeasurableproof · cited by 21
- Filter.comap_cocompact_leproof · cited by 7
- intervalIntegral.integral_deriv_smul_comp''proof · cited by 4
- ContinuousWithinAt.mem_closure_imageproof · cited by 4
- AntilipschitzWith.isBounded_of_image2_leftproof · cited by 3
- Set.subsingleton_of_imageproof · cited by 3
- Finsupp.lmapDomain_supportedproof · cited by 2
- Topology.IsClosedEmbedding.normalSpaceproof · cited by 2
- NumberField.mixedEmbedding.fundamentalCone.normLeOne_eq_preimage_imageproof · cited by 2
- ContDiffWithinAt.comp_of_mem_nhdsWithin_imageproof · cited by 2