Theorems · Theorem · combinatorics

Equiv.Perm.exists_extending_pair

∀ {α : Type u_1} {β : Type u_2} [Finite α] (f g : α → β),
  Function.Injective f → Function.Injective g → ∃ σ, ∀ (a : α), σ (f a) = g a

Given two injective functions f and g from a finite type α to any type β, there exists a permutation of β that maps f to g.

Defined in

Mathlib.Logic.Equiv.Fintype

Cited by

2 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Finite