English
Let s ⊆ α be a finite set with f mapping s into t and injOn f on s, and card α = card t. Then there exists a bijection g: α ≃ t extending f on s, i.e., ∀ i ∈ s, g(i) = f(i).
Русский
Пусть s ⊆ α и отображение f: α → β ограничено на s и инъективно на s, а кардинал α равен кардиналу t; тогда существует биекция g: α ≃ t, такая что g(i) = f(i) для всех i ∈ s.
LaTeX
$$$$\\exists g : α \\simeq t,\\; \\forall i \\in s,\\; (g(i) : β) = f(i).$$$$
Lean4
/-- Any injection from a set `s` in a fintype `α` to a finset `t` of the same cardinality as `α`
can be extended to a bijection between `α` and `t`. -/
theorem exists_equiv_extend_of_card_eq [Fintype α] {t : Finset β} (hαt : Fintype.card α = #t) {s : Set α} {f : α → β}
(hfst : s.MapsTo f t) (hfs : Set.InjOn f s) : ∃ g : α ≃ t, ∀ i ∈ s, (g i : β) = f i := by
classical
let s' : Finset α := s.toFinset
have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using hfst
have hfs' : Set.InjOn f s' := by simpa [s'] using hfs
obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
refine ⟨g, fun i hi => ?_⟩
apply hg
simpa [s'] using hi
