Library sset1

• Fundamental set theory
  • Axioms
  • Tactics
  • Constructions
  • Little
  • Image
  • Complement
  • Union
  • Powerset
  • Intersection
  • Ordered Pair
  • Cartesian products of two sets
  • Functional graphs

Library sset2

• Theory of Sets EII-3 Correspondences
  • EII-3-1 Graphs et correspondences
  • Additional lemmas
  • EII-3-2 Inverse of a correspondence
  • EII-3-3 Composition of two correspondences
  • EII-3-4 Functions
  • EII-3-5 Restrictions and extensions of functions
  • EII-3-6 Definition of a function by means of a term
  • EII-3-7 Composition of two functions. Inverse function
  • EII-3-8 Retractions and sections
  • EII-3-9 Functions of two arguments

Library sset3

• Theory of Sets: EII-4 Union and intersection of a family of sets
  • EII-4-1 Definition of the union and intersection of a family of sets
  • EII-4-2 Properties of union and intersection
  • EII-4-3 Images of a union and an intersection
  • EII-4-4 complement of unions and intersections
  • EII-4-5 union and intersection of two sets
  • EII-4-6 Coverings
  • EII-4-7 Partitions
  • EII-4-8 Sum of a family of sets
• EII-5 Product of a family of sets
  • EII-5-1 The axiom of the set of subsets
  • EII-5-2 Set of mappings of one set into another
  • EII-5-3 Definition of the product of a family of sets
  • EII-5-4 Partial products
  • EII-5-5 associativity of products of sets
  • EII-5-6 distributivity formulae
  • EII-5-7 Extensions of mappings to products

Library sset4

• Theory of Sets EII-6 Equivalence relations
  • EII-6-1 Definition of an equivalence relation
  • EII-6-2 Equivalence classes; quotient set
  • EII-6-3 Relations compatible with an equivalence relation
  • EII-6-4 saturated subsets
  • EII-6-5 Mappings compatible with equivalence relations
  • EII-6-6 Inverse image of an equivalence relation; induced equivalence relation
  • EII-6-7 Quotients of equivalence relations
  • EII-6-8 Product of two equivalence relations

Library sset5

• Theory of Sets EIII-1 Order relations. Ordered sets
  • EIII-1-1 Definition of an order relation
  • Preorder relations
  • Notation and terminology
  • Ordered subsets. Product of ordered sets
  • Increasing mappings
  • Maximal and minimal elements
  • Greatest element and least element
  • Upper and lower bounds
  • Least upper bound and greatest lower bound
  • Directed sets
  • Lattices
  • Totally ordered sets
  • Intervals

Library sset6

• Theory of Sets EIII-2 Well ordered sets
  • EIII-2-1 Segments of a well-ordered set
  • EIII-2-2 The principle of transfinite induction
  • EIII-2-3 Zermelo's theorem
  • EIII-2-4 Inductive sets
  • EIII-2-5 Isomorphisms of well-ordered sets
  • EIII-2-6 Lexicographic Products

Library sset7

• Theory of Sets EIII-3 Equipotents Sets. Cardinals
  • Ordinals
  • EIII-3-1 The cardinal of a set
  • EIII-3-2 Order relation between cardinals

Library sset8

• Theory of Sets EIII-4 Natural integers. Finite sets
  • EIII-3-3 Operations on Cardinals
  • EIII-3-4 Properties of the cardinals 0 and 1
  • EIII-3-5 Exponentiation of cardinals
  • EIII-3-6 Order relation and operations on cardinals
  • EIII-4-1 Definition of integers
  • EIII-6-1 The set of natural integers
  • EIII-4-3 The principle of induction
  • EIII-4-4 Finite subsets of ordered sets
  • EIII-4-5 Properties of finite character

Library sset9

• Theory of Sets EIII-5 Properties of integers
  • EIII-5-1 Operations on integers and finite sets
  • EIII-5-2 Strict inequalities between integers
  • EIII-5-3 Intervals in sets of integers
  • EIII-5-4 Finite sequences
  • EIII-5-5 Characteristic functions on sets
  • EIII-5-6 Euclidean Division
  • EIII-5-7 Expansion to base b
  • EIII-5-8 Combinatorial analysis

Library sset10

• Theory of Sets EIII-6 Infinite sets
  • EIII-6-1 The set of natural integers
  • EIII-6-2 Definition of mappings by induction
  • EIII-6-3 Properties of infinite cardinals
  • EIII-6-4 Countable sets
  • EIII-6-5 Stationary sequences

Library sset10b

• Theory of Sets EIII-6 Infinite sets
  • The set of rational integers
  • Opposite
  • Absolute value
  • Ordering on Z
  • Addition
  • Multiplication
  • The sign function
  • Division
  • Ideals
  • Gcd

Library sset11

• Theory of Sets : Ordinals
  • Sums and products of orders
  • ordinal sum and product
  • Properties of ordering
  • Least upper bound
  • Subtraction
  • Ordinal division

Library sset12

• Theory of Sets : Ordinals
  • Normal ordinal functional symbols
  • Indexing a collection of ordinals
  • Indecomposable ordinals
  • Definition by induction for the exponential
  • Ordinal power

Library sset13

• Theory of Sets : Ordinals
  • Cantor normal form
  • General Cantor Normal Form

Library sset14

• Theory of Sets : Ordinals
  • Epsilon ordinals
  • Initial ordinals
  • cardinal cofinality
  • Inaccessible cardinals

Library sset15

• Theory of Sets : Ordinals

Library sset16

• Theory of Sets : Ordinals

Library ssete1

• • Bourbaki Sets 1 Exercises
  • Section 1
  • Section 2
  • Section 3
  • Section 4
  • Section 5
  • Section 6

Library ssete2

• Theory of Sets : Exercises
  • Section 1

Library ssete3

• Theory of Sets : Exercises sections 2 and 3
  • Section 3

Library ssete4

• Theory of Sets : Exercises sections 4

Library ssete5

• • Bourbaki Exercices
  • Section 6
  • Exercises of Section 6

Library ssete6

• Theory of Sets : Exercises sections 6
  • The von Neuman ordinals
  • Bourbaki Exercices Order Types

Library ssete7

Library ssete8

Library ssete9

• prelude
  • Example 1
  • Example 2
  • Example 3
  • More on accessiblity
• The type T1
  • Equality
  • Order on T1
  • Normal form
  • Successor
  • Addition
  • Limits
    • Definition
    • The normal form
    • Realizing the limit
    • Normal functions
  • multiplication
    • Preparation of the exponention
    • Normality of multiplication
  • Exponentiation
    • Existence and uniqueness of the Cantor Normal Form
    • Basic Properties
• The type T2
  • Definition and Equality
  • Order
  • Normal form
  • Successor and predecessor
  • Addition
  • The function phi
• Ackermann
  • Comparison
  • Normal form
  • Successor Predecessor
  • Addition
  • limit
  • additive principal