Mathlib Map

Theorems · Theorem · order theory

sigma_mk_injective

∀ {α : Type u_1} {β : α → Type u_4} {i : α}, Function.Injective (Sigma.mk i)
Defined in
Mathlib.Data.Sigma.Basic
Cited by
27 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Function.Embedding.sigmaMk · cited by 25Embedding.sigmaMkHasSum.sigma · cited by 8HasSum.sigmaHasProd.sigma · cited by 5HasProd.sigmaisOpenMap_sigmaMk · cited by 5isOpenMap_sigmaMkTopology.IsOpenEmbedding.sigmaMk · cited by 5IsOpenEmbedding.sigmaMkFinset.sigma_preimage_mk · cited by 3Finset.sigma_preimage_mkSummable.sigma_factor · cited by 3Summable.sigma_factorTopology.IsClosedEmbedding.sigmaMk · cited by 3IsClosedEmbedding.sigmaMkFunction.Injective.sigma_map · cited by 2Injective.sigma_mapMultipliable.sigma_factor · cited by 2Multipliable.sigma_factorisClosedMap_sigmaMk · cited by 2isClosedMap_sigmaMkMeasureTheory.Measure.infinitePi_map_piCurry_symm · cited by 2Measure.infinitePi_map_pi…Sigma.isConnected_iff · cited by 2Sigma.isConnected_iffHasCardinalLT.exists_regular_cardinal_forall · cited by 1HasCardinalLT.exists_regu…Topology.isInducing_sigmaMap · cited by 1Topology.isInducing_sigma…sigma_mk_injectiveCITED 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 by28

Results whose statement or proof uses this declaration.