English
Given a finite α, a target Finset t with card α = card t, and an injection f : α → β defined on s ⊆ α that is injective on s and lands in t, there exists a bijection g: α ≃ t extending f on s, i.e., ∀ i ∈ s, g(i) = f(i).
Русский
Для конечного α и цели t с равной мощностью, и для вложенной инекции f на s ⊆ α, существует биекция g: α ≃ t, совпадающая с f на s.
LaTeX
$$$$\\exists g : \\alpha \\simeq t, \\; \\forall i \\in s,\\; g(i) = f(i).$$$$
Lean4
/-- Any injection from a finset `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 α] [DecidableEq β] {t : Finset β} (hαt : Fintype.card α = #t)
{s : Finset α} {f : α → β} (hfst : Finset.image f s ⊆ t) (hfs : Set.InjOn f s) :
∃ g : α ≃ t, ∀ i ∈ s, (g i : β) = f i := by
classical
induction s using Finset.induction generalizing f with
| empty =>
obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]
use e
simp
| insert a s has H => ?_
have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
obtain ⟨g', hg'⟩ := H hfst' hfs'
have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
simp_rw [mem_insert]
rintro i (rfl | hi)
· simp
rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
·
exact
ne_of_apply_ne Subtype.val
(ne_of_eq_of_ne (hg' _ hi) <|
hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)
· exact g'.injective.ne (ne_of_mem_of_not_mem hi has)
