Theorems · Definition · logic and foundations
Set.rangeFactorization
{α : Type u} → {ι : Sort u_1} → (f : ι → α) → ι → ↑(Set.range f)Any map f : ι → α factors through a map rangeFactorization f : ι → range f.
- Defined in
- Mathlib.Data.Set.Operations
- Cited by
- 56 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.Elemstatement · cited by 7,166
- Set.rangestatement · cited by 4,705
- Set.mem_range_selfproof · cited by 328
Cited by59
Results whose statement or proof uses this declaration.
- Topology.IsStrictMapproof · cited by 45
- Set.rangeFactorization_surjectivestatement and proof · cited by 20
- Cardinal.mk_range_le_liftproof · cited by 15
- stronglyMeasurable_iff_measurable_separableproof · cited by 13
- Topology.IsQuotientMap.isStrictMap_iffproof · cited by 8
- tendsto_atTop_isLUBproof · cited by 7
- Topology.IsEmbedding.aestronglyMeasurable_comp_iffproof · cited by 6
- Topology.isStrictMap_iff_isQuotientMap_rangeFactorizationstatement · cited by 5
- Set.rightInverse_rangeSplittingstatement and proof · cited by 4
- Continuous.rangeFactorizationstatement · cited by 3
- Set.leftInverse_rangeSplittingstatement · cited by 3
- Function.Exact.iff_rangeFactorizationstatement · cited by 3