Sierpinski.Prelim

• Preliminaries
  • Logical Basis
  • Subtypes
  • Injections
  • Proof that X * X embeds into (X -> Prop) -> Prop
  • Infinite Types
  • Bijections
  • Inclusion

Sierpinski.Hartogs

• Hartogs Numbers
  • Well-Orders as Inclusion Systems
  • Order-Embeddings
  • Order-Isomorphisms
  • Relational Variants
  • Segments
  • Ordinals
  • Wellfoundedness of Ordinals
  • Hartogs Numbers
  • HN does not inject into X

Sierpinski.Sierpinski

• Sierpinski's Theorem
  • Constructive bijections
  • Bijections relying on unique choice
  • Sierpinski's Theorem
  • Main result

Sierpinski.Variant

• Proof Variant without Unique Choice
  • Reformulation of relevant notions and lemmas
  • Main result
  • Diaconescu