Mathlib Map

Theorems · Theorem

Prod.fst_surjective

∀ {α : Type u_1} {β : Type u_2} [h : Nonempty β], Function.Surjective Prod.fst
Defined in
Mathlib.Data.Prod.Basic
Cited by
22 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
Nonempty
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Ideal.ideal_prod_eq · cited by 4Ideal.ideal_prod_eqisCyclic_left_of_prod · cited by 2isCyclic_left_of_prodMonoid.exponent_prod · cited by 2Monoid.exponent_prodisAddCyclic_left_of_prod · cited by 2isAddCyclic_left_of_prodisOpenQuotientMap_fst · cited by 2isOpenQuotientMap_fstNonUnitalSubsemiring.range_fst · cited by 1NonUnitalSubsemiring.rang…AddSubsemigroup.srange_fst · cited by 1AddSubsemigroup.srange_fstAddMonoid.exponent_prod · cited by 1AddMonoid.exponent_prodIsHomeomorphicTrivialFiberBundle.surjective_proj · cited by 1IsHomeomorphicTrivialFibe…Ideal.map_fst_prod · cited by 1Ideal.map_fst_prodFinite.prod_left · cited by 1Finite.prod_leftSubsemigroup.srange_fst · cited by 1Subsemigroup.srange_fstProd.range_fst · cited by 1Prod.range_fstSubmonoid.mrange_fst · cited by 1Submonoid.mrange_fstModule.finitePresentation_of_split_exact · cited by 1Module.finitePresentation…Prod.fst_surjectiveCITED 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 by22

Results whose statement or proof uses this declaration.