Mathlib Map

Theorems · Theorem

Function.Surjective.of_comp

∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α},
  Function.Surjective (f ∘ g) → Function.Surjective f
Defined in
Mathlib.Logic.Function.Basic
Cited by
30 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Function.Surjective.of_comp_iff · cited by 7Surjective.of_comp_iffdualTensorHom_bijective · cited by 6dualTensorHom_bijectiveLinearMap.surjective_of_comp_eq_id · cited by 5LinearMap.surjective_of_c…Topology.IsCoinducing.isConnected_preimage_of_isClosed · cited by 3IsCoinducing.isConnected_…LaurentSeries.valuation_compare · cited by 3LaurentSeries.valuation_c…dualTensorHom_bijective_of_comp_eq_id_right · cited by 3dualTensorHom_bijective_o…Topology.IsQuotientMap.of_comp · cited by 3IsQuotientMap.of_compIsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective · cited by 2HeightOneSpectrum.valuedA…MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing · cited by 2MvPolynomial.comp_C_integ…SimpleGraph.card_le_chromaticNumber_iff_forall_surjective · cited by 2SimpleGraph.card_le_chrom…Topology.IsQuotientMap.of_comp_of_isCoinducing · cited by 2IsQuotientMap.of_comp_of_…PrimeSpectrum.finite_of_toPiLocalization_surjective · cited by 1PrimeSpectrum.finite_of_t…Module.Free.bijective_algebraMap_of_finrank_eq_one · cited by 1Free.bijective_algebraMap…AlgebraicGeometry.Surjective.of_comp · cited by 1Surjective.of_compIsOpenQuotientMap.of_comp · cited by 1IsOpenQuotientMap.of_compSurjective.of_compCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by30

Results whose statement or proof uses this declaration.