English
If s is finite and s.encard ≤ t.encard, there exists f : α → β with s ⊆ f^{-1}' t and InjOn f s.
Русский
Если s конечно и s.encard ≤ t.encard, существует f : α → β с s ⊆ f^{-1}' t и InjOn f s.
LaTeX
$$$\\exists f : \\alpha \\to \\beta,\\ s \\subseteq f^{-1}' t \\land InjOn f s$$$
Lean4
theorem exists_injOn_of_encard_le [Nonempty β] {s : Set α} {t : Set β} (hs : s.Finite) (hle : s.encard ≤ t.encard) :
∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s := by
classical
obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
· simp
· exact (encard_ne_top_iff.mpr hs h).elim
obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)
have hle' : (s \ { a }).encard ≤ (t \ { b }).encard := by
rwa [← WithTop.add_le_add_iff_right WithTop.one_ne_top, encard_diff_singleton_add_one has,
encard_diff_singleton_add_one hbt]
obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.diff hle'
simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s
use Function.update f₀ a b
rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
simp only [mem_diff, mem_singleton_iff, insert_diff_singleton, subset_def, mem_insert_iff, mem_preimage,
Function.update_apply, forall_eq_or_imp, ite_true, and_imp, mem_image, ite_eq_left_iff, not_exists, not_and,
not_forall, exists_prop, and_iff_right hbt]
refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
· rintro x hx; split_ifs with h
· assumption
· exact (hf₀s x hx h).1
exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_of_ne])
termination_by encard s
