English
Given an embedding f: s → β with a witness that the complements are in bijection, there exists a bijection g: α ≃ β extending f on s.
Русский
Для вложения f: s → β и существования биекции между дополнениями, существует биекция g: α ≃ β, которая расширяет f на s.
LaTeX
$$$\\exists g: \\alpha \\cong \\beta, \\forall x:\\, s, \\; g(x) = f(x)$$$
Lean4
theorem extend_function {α β : Type*} {s : Set α} (f : s ↪ β) (h : Nonempty ((sᶜ : Set α) ≃ ((range f)ᶜ : Set β))) :
∃ g : α ≃ β, ∀ x : s, g x = f x := by
classical
have := h; obtain ⟨g⟩ := this
let h : α ≃ β :=
(Set.sumCompl (s : Set α)).symm.trans ((sumCongr (Equiv.ofInjective f f.2) g).trans (Set.sumCompl (range f)))
refine ⟨h, ?_⟩; rintro ⟨x, hx⟩; simp [h, Set.sumCompl_symm_apply_of_mem, hx]
