Mathlib Map

Theorems · Theorem

Function.Injective.piMap

∀ {ι : Sort u_4} {α : ι → Sort u_5} {β : ι → Sort u_6} {f : (i : ι) → α i → β i},
  (∀ (i : ι), Function.Injective (f i)) → Function.Injective (Pi.map f)
Defined in
Mathlib.Logic.Function.Basic
Cited by
5 results in Mathlib
Foundations
Depth 5 from the axioms · uses Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Function.Injective.comp_left · cited by 15Injective.comp_leftPi.map_injective · cited by 5Pi.map_injectiveTopology.IsEmbedding.piMap · cited by 3IsEmbedding.piMapAlgebraicGeometry.mono_pushoutSection_of_iSup_eq · cited by 2AlgebraicGeometry.mono_pu…Function.Bijective.piMap · cited by 0Bijective.piMapPi.map · cited by 60Pi.mapInjective.piMapCITED BYCITES

Cites1

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

  • Pi.mapstatement and proof · cited by 60

Cited by5

Results whose statement or proof uses this declaration.