The Cantor–Schröder–Bernstein–Escardó theorem

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-05-20.
Last modified on 2025-10-29.

module foundation.cantor-schroder-bernstein-escardo where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.cantor-schroder-bernstein-decidable-embeddings
open import foundation.decidable-propositions
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.injective-maps
open import foundation.law-of-excluded-middle
open import foundation.propositions
open import foundation.universe-levels

open import foundation-core.embeddings
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.propositional-maps
open import foundation-core.sets

Idea

The classical Cantor–Schröder–Bernstein theorem asserts that from any pair of injective maps f : A → B and g : B → A we can construct a bijection between A and B. In a recent generalization, Escardó proved that a Cantor–Schröder–Bernstein theorem also holds for ∞-groupoids. His generalization asserts that given two types that embed into each other, then the types are equivalent. [Esc21]

Theorem

The Cantor-Schröder-Bernstein-Escardó theorem

module _
  {l1 l2 : Level} (lem : LEM (l1 ⊔ l2))
  {A : UU l1} {B : UU l2}
  where abstract

  Cantor-Schröder-Bernstein-Escardó' :
    {f : A → B} {g : B → A} →
    is-emb g → is-emb f → A ≃ B
  Cantor-Schröder-Bernstein-Escardó' {f} {g} G F =
    Cantor-Schröder-Bernstein-WLPO'
      ( λ P → lem (Π-Prop ℕ (prop-Decidable-Prop ∘ P)))
      ( G , λ y → lem (fiber g y , is-prop-map-is-emb G y))
      ( F , λ y → lem (fiber f y , is-prop-map-is-emb F y))

  Cantor-Schröder-Bernstein-Escardó :
    A ↪ B → B ↪ A → A ≃ B
  Cantor-Schröder-Bernstein-Escardó (f , F) (g , G) =
    Cantor-Schröder-Bernstein-Escardó' G F

Corollaries

The Cantor–Schröder–Bernstein theorem

module _
  {l1 l2 : Level} (lem : LEM (l1 ⊔ l2))
  (A : Set l1) (B : Set l2)
  where abstract

  Cantor-Schröder-Bernstein :
    injection (type-Set A) (type-Set B) →
    injection (type-Set B) (type-Set A) →
    (type-Set A) ≃ (type-Set B)
  Cantor-Schröder-Bernstein f g =
    Cantor-Schröder-Bernstein-Escardó lem
      ( emb-injection B f)
      ( emb-injection A g)

References

[Esc21]
Martín Hötzel Escardó. The Cantor–Schröder–Bernstein Theorem for ∞-groupoids. Journal of Homotopy and Related Structures, 16(3):363–366, 09 2021. arXiv:2002.07079, doi:10.1007/s40062-021-00284-6.
[Esc]
Martín Hötzel Escardó and contributors. TypeTopology. GitHub repository. Agda development. URL: https://github.com/martinescardo/TypeTopology.
[Wie]
Freek Wiedijk. Formalizing 100 theorems. URL: https://www.cs.ru.nl/~freek/100/.

See also

The Cantor–Schröder–Bernstein–Escardó theorem holds constructively for many notions of finite type, including

Recent changes