Theorems · Theorem · order theory
Set.preimage_range
∀ {α : Type u_1} {β : Type u_2} (f : α → β), f ⁻¹' Set.range f = Set.univ- Defined in
- Mathlib.Data.Set.Image
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Set.preimagestatement · cited by 4,946
- Set.rangestatement · cited by 4,705
- Set.univstatement · cited by 3,945
- Set.mem_range_selfproof · cited by 328
- Set.eq_univ_of_forallproof · cited by 80
Cited by38
Results whose statement or proof uses this declaration.
- Subtype.coe_preimage_selfproof · cited by 46
- MeasurableEmbedding.map_applyproof · cited by 16
- MvPolynomial.mem_range_map_iff_coeffs_subsetproof · cited by 5
- Affine.Simplex.touchpoint_mem_affineSpan_simplexproof · cited by 4
- AlgebraicGeometry.Scheme.Hom.preimage_opensRangeproof · cited by 3
- WithBot.preimage_coe_Ioi_botproof · cited by 3
- WithTop.preimage_coe_Iio_topproof · cited by 3
- Set.preimage_eq_emptyproof · cited by 3
- MeasurableEmbedding.sigmaFinite_mapproof · cited by 3
- Affine.Simplex.closedInterior_face_subset_closedInteriorproof · cited by 2
- Nat.card_range_of_injectiveproof · cited by 2
- Affine.Simplex.abs_inner_vsub_altitudeFoot_lt_mulproof · cited by 2