English
Given injections f: α → β and g: β → α with a pointwise relation R preserved by f and g, there exists a function h: α → β that is injective and surjective (bijective) and satisfies R(a, h(a)).
Русский
Пусть существуют инъекции f: α → β и g: β → α и некоорая связь R, сохраняемая f и g по точкам. Тогда существует биекция h: α → β такая, что R(a, h(a)) для всех a.
LaTeX
$$$\exists h: \alpha \to \beta, \mathrm{Bijective}(h) \land \forall a:\alpha, R(a, h(a)).$$$
Lean4
/-- **The Schröder-Bernstein Theorem**:
Given injections `α → β` and `β → α` that satisfy a pointwise property `R`, we can get a bijection
`α → β` that satisfies that same pointwise property. -/
theorem schroeder_bernstein_of_rel {f : α → β} {g : β → α} (hf : Function.Injective f) (hg : Function.Injective g)
(R : α → β → Prop) (hp₁ : ∀ a : α, R a (f a)) (hp₂ : ∀ b : β, R (g b) b) :
∃ h : α → β, Bijective h ∧ ∀ a : α, R a (h a) := by
classical
rcases isEmpty_or_nonempty β with hβ | hβ
· have : IsEmpty α := Function.isEmpty f
exact ⟨_, ((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm).bijective, by simp⟩
set F : Set α →o Set α :=
{ toFun := fun s => (g '' (f '' s)ᶜ)ᶜ
monotone' := fun s t hst => by dsimp at hst ⊢; gcongr }
set s : Set α := F.lfp
have hs : (g '' (f '' s)ᶜ)ᶜ = s := F.map_lfp
have hns : g '' (f '' s)ᶜ = sᶜ := compl_injective (by simp [hs])
set g' := invFun g
have g'g : LeftInverse g' g := leftInverse_invFun hg
have hg'ns : g' '' sᶜ = (f '' s)ᶜ := by rw [← hns, g'g.image_image]
set h : α → β := s.piecewise f g'
have : Surjective h := by rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]
have : Injective h := by
refine (injective_piecewise_iff _).2 ⟨hf.injOn, ?_, ?_⟩
· intro x hx y hy hxy
obtain ⟨x', _, rfl⟩ : x ∈ g '' (f '' s)ᶜ := by rwa [hns]
obtain ⟨y', _, rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
rw [g'g _, g'g _] at hxy
rw [hxy]
· intro x hx y hy hxy
obtain ⟨y', hy', rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
rw [g'g _] at hxy
exact hy' ⟨x, hx, hxy⟩
refine ⟨h, ⟨‹Injective h›, ‹Surjective h›⟩, fun a ↦ ?_⟩
simp only [h, Set.piecewise, g']
split
· exact hp₁ a
· have : g (invFun g a) = a := by
have : a ∈ g '' (f '' s)ᶜ := by grind
obtain ⟨x, _, hx⟩ := mem_image _ _ _ |>.mp this
exact Function.invFun_eq ⟨x, hx⟩
grind
