Theorems · Theorem · order theory

Function.Injective.sigma_map

∀ {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁ → Type u_5} {β₂ : α₂ → Type u_6} {f₁ : α₁ → α₂}
  {f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)},
  Function.Injective f₁ → (∀ (a : α₁), Function.Injective (f₂ a)) → Function.Injective (Sigma.map f₁ f₂)

Defined in: Mathlib.Data.Sigma.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 10 from the axioms · uses propext

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites3

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

Sigma.mapstatement and proof · cited by 29
sigma_mk_injectiveproof · cited by 27
Sigma.mk.inj_iffproof · cited by 4

Cited by2

Results whose statement or proof uses this declaration.

FirstOrder.Language.card_functions_sum_skolem₁_leproof · cited by 1
Function.Injective.sigma_map_iffproof · cited by 1