Theorems · Theorem

Prod.map_bijective

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ},
  Function.Bijective (Prod.map f g) ↔ Function.Bijective f ∧ Function.Bijective g

Defined in: Mathlib.Data.Prod.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 8 from the axioms · uses propext, Classical.choice
Assumes: Nonempty Nonempty

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Function.Bijectivestatement · cited by 863
Nonempty.mapproof · cited by 101
Iff.andproof · cited by 33
Prod.map_injectiveproof · cited by 7
Prod.map_surjectiveproof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.