Theorems · Theorem · order theory
Function.Surjective.range_eq
∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α}, Function.Surjective f → Set.range f = Set.univAlias of the reverse direction of Set.range_eq_univ.
- Defined in
- Mathlib.Data.Set.Image
- Cited by
- 70 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.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Set.rangestatement · cited by 4,705
- Set.univstatement · cited by 3,945
- Set.range_eq_univproof · cited by 50
Cited by71
Results whose statement or proof uses this declaration.
- Function.Surjective.denseRangeproof · cited by 21
- Filter.map_comap_of_surjectiveproof · cited by 11
- StrictMono.orderIsoOfSurjectiveproof · cited by 8
- Finsupp.mapRange_surjectiveproof · cited by 7
- IsUniformInducing.completeSpace_congrproof · cited by 6
- Topology.IsEmbedding.aestronglyMeasurable_comp_iffproof · cited by 6
- Function.Surjective.preimage_subset_preimage_iffproof · cited by 6
- Bornology.IsVonNBounded.imageproof · cited by 5
- AmpleSet.imageproof · cited by 4
- OrderIso.range_eqproof · cited by 3
- AlgebraicGeometry.compactSpace_iff_existsproof · cited by 2
- Filter.map_piMap_piproof · cited by 2