Exercise 4.24 (Scott 1981, PRG-19, Lecture IV) — Schröder–Bernstein via a fixed

point

(For set theorists.) Let f : A → B and g : B → A be one-one (injective, not necessarily onto). Then there is a one-one correspondence h : A ≃ B (schroeder_bernstein).

Following Tarski's hint, work in the power-set domain P A (a complete lattice) and take a fixed point X of the monotone operator

T(X) = (A − g(B)) ∪ g(f(X)),

which exists by Knaster–Tarski (Exercise 4.14 / 4.13(2), here lfpSet). With X = T(X) fixed, define

h(a) = f(a) if a ∈ X, h(a) = g⁻¹(a) if a ∉ X

— well-defined because a ∉ X = T(X) forces a ∈ g(B) (it is not in (A − g(B))), so a has a unique g-preimage (mem_range_of_not_mem). The map h is:

• injective (sbFun_injective): within X, by injectivity of f; outside X, by injectivity of g; the mixed case is impossible — f(a₁) = g⁻¹(a₂) would put a₂ = g(f(a₁)) ∈ g(f(X)) ⊆ X;
• surjective (sbFun_surjective): for b ∈ B, if g(b) ∉ X then h(g(b)) = b; if g(b) ∈ X then g(b) ∈ g(f(X)), so g(b) = g(f(a)) with a ∈ X, whence b = f(a) = h(a).

Packaged as the equivalence schroederBernsteinEquiv. This is a set theorists' exercise and is inherently classical; the construction of h uses Classical.choice (the g-preimage), exactly as the statement demands.

def Domain.Neighborhood.Exercise424.sbOp {A : Type u_1} {B : Type u_2} (f : A → B) (g : B → A) (X : Set A) : Set A

Tarski's operator T(X) = (A − g(B)) ∪ g(f(X)) on P A.

Equations

• Domain.Neighborhood.Exercise424.sbOp f g X = (Set.range g)ᶜ ∪ g '' f '' X

theorem Domain.Neighborhood.Exercise424.sbOp_monotone {A : Type u_1} {B : Type u_2} (f : A → B) (g : B → A) : Monotone (sbOp f g)

def Domain.Neighborhood.Exercise424.sbSet {A : Type u_1} {B : Type u_2} (f : A → B) (g : B → A) : Set A

The Tarski fixed point X with X = (A − g(B)) ∪ g(f(X)) (lfpSet, Exercise 4.14).

Equations

• Domain.Neighborhood.Exercise424.sbSet f g = Domain.Neighborhood.Exercise414.lfpSet (Domain.Neighborhood.Exercise424.sbOp f g)

theorem Domain.Neighborhood.Exercise424.sbSet_isFixed {A : Type u_1} {B : Type u_2} (f : A → B) (g : B → A) : sbOp f g (sbSet f g) = sbSet f g

theorem Domain.Neighborhood.Exercise424.mem_range_of_not_mem {A : Type u_1} {B : Type u_2} {f : A → B} {g : B → A} {a : A} (ha : ¬a ∈ sbSet f g) : a ∈ Set.range g

Anything outside the fixed set X lies in the range of g (so it has a g-preimage).

noncomputable def Domain.Neighborhood.Exercise424.sbFun {A : Type u_1} {B : Type u_2} (f : A → B) (g : B → A) (a : A) : B

Exercise 4.24 (Scott 1981, PRG-19). Tarski's bijection h : A → B: f on the fixed set X, and the g-inverse off it.

Equations

• Domain.Neighborhood.Exercise424.sbFun f g a = if ha : a ∈ Domain.Neighborhood.Exercise424.sbSet f g then f a else Classical.choose ⋯

theorem Domain.Neighborhood.Exercise424.sbFun_mem {A : Type u_1} {B : Type u_2} {f : A → B} {g : B → A} {a : A} (ha : a ∈ sbSet f g) : sbFun f g a = f a

theorem Domain.Neighborhood.Exercise424.g_sbFun_not_mem {A : Type u_1} {B : Type u_2} {f : A → B} {g : B → A} {a : A} (ha : ¬a ∈ sbSet f g) : g (sbFun f g a) = a

Off the fixed set, h(a) is a genuine g-preimage of a: g(h(a)) = a.

theorem Domain.Neighborhood.Exercise424.g_f_mem_of_mem {A : Type u_1} {B : Type u_2} {f : A → B} {g : B → A} {a : A} (ha : a ∈ sbSet f g) : g (f a) ∈ sbSet f g

g(f(a)) ∈ X whenever a ∈ X (the g(f(X)) ⊆ T(X) = X half).

theorem Domain.Neighborhood.Exercise424.sbFun_injective {A : Type u_1} {B : Type u_2} {f : A → B} {g : B → A} (hf : Function.Injective f) : Function.Injective (sbFun f g)

theorem Domain.Neighborhood.Exercise424.sbFun_surjective {A : Type u_1} {B : Type u_2} {f : A → B} {g : B → A} (hg : Function.Injective g) : Function.Surjective (sbFun f g)

theorem Domain.Neighborhood.Exercise424.schroeder_bernstein {A : Type u_1} {B : Type u_2} {f : A → B} {g : B → A} (hf : Function.Injective f) (hg : Function.Injective g) : ∃ (h : A → B), Function.Bijective h

Exercise 4.24 (Scott 1981, PRG-19) — Schröder–Bernstein. Injections f : A → B and g : B → A yield a bijection A → B.

noncomputable def Domain.Neighborhood.Exercise424.schroederBernsteinEquiv {A : Type u_1} {B : Type u_2} {f : A → B} {g : B → A} (hf : Function.Injective f) (hg : Function.Injective g) : A ≃ B

Exercise 4.24 (Scott 1981, PRG-19). The one-one correspondence as an Equiv A ≃ B.

Equations

• Domain.Neighborhood.Exercise424.schroederBernsteinEquiv hf hg = Equiv.ofBijective (Domain.Neighborhood.Exercise424.sbFun f g) ⋯