Theorems · Theorem · order theory
Set.image_preimage_eq
∀ {α : Type u_1} {β : Type u_2} {f : α → β} (s : Set β), Function.Surjective f → f '' f ⁻¹' s = s- Defined in
- Mathlib.Data.Set.Image
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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 and proof · cited by 5,609
- Set.preimagestatement and proof · cited by 4,946
- Set.Subset.antisymmproof · cited by 213
- Set.image_preimage_subsetproof · cited by 75
Cited by38
Results whose statement or proof uses this declaration.
- Function.Surjective.image_preimageproof · cited by 16
- MulAction.IsPreprimitive.of_surjectiveproof · cited by 8
- AlgebraicGeometry.Scheme.Hom.support_kerproof · cited by 6
- AddAction.IsPreprimitive.of_surjectiveproof · cited by 4
- Measurable.measurableSet_preimage_iff_of_surjectiveproof · cited by 3
- compact_open_separated_add_leftproof · cited by 2
- Topology.IsCoinducing.image_connectedComponentproof · cited by 2
- IsSemilinearSet.interproof · cited by 2
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_isoproof · cited by 2
- Disjoint.of_preimageproof · cited by 2
- isSemilinearSet_setOfPred_eqproof · cited by 1
- AlgebraicGeometry.Scheme.isoSpec_image_zeroLocusproof · cited by 1