Theorems · Theorem · order theory
Function.Surjective.range_comp
∀ {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} {f : ι → ι'},
Function.Surjective f → ∀ (g : ι' → α), Set.range (g ∘ f) = Set.range g- Defined in
- Mathlib.Data.Set.Image
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 6 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.extproof · cited by 2,266
- Function.Surjective.existsproof · cited by 53
Cited by18
Results whose statement or proof uses this declaration.
- Set.Countable.exists_eq_rangeproof · cited by 17
- EquivLike.range_compproof · cited by 15
- Function.Surjective.iSup_compproof · cited by 9
- Topology.IsQuotientMap.isStrictMap_iffproof · cited by 8
- Function.Surjective.iInf_compproof · cited by 7
- MeasureTheory.analyticSet_range_of_polishSpaceproof · cited by 6
- Cardinal.mk_biUnion_le_of_le_liftproof · cited by 3
- Function.Surjective.comp_exact_iff_exactproof · cited by 2
- Function.semiconj_of_isLUBproof · cited by 2
- denseRange_zpow_iff_surjectiveproof · cited by 1
- denseRange_zsmul_iff_surjectiveproof · cited by 1
- KaehlerDifferential.kerTotal_mapproof · cited by 1