Von Neumann ordinals #

This file works towards the development of von Neumann ordinals, i.e. transitive sets, well-ordered under . We currently only have an initial development of transitive sets.

Further development can be found on the branch von_neumann_v2.

Definitions #

Todo #

A transitive set is one where every element is a subset.

Instances For
    theorem ZFSet.isTransitive_iff_mem_trans {z : ZFSet} :
    ZFSet.IsTransitive z ∀ {x y : ZFSet}, x yy zx z
    theorem ZFSet.IsTransitive.mem_trans {z : ZFSet} :
    ZFSet.IsTransitive z∀ {x y : ZFSet}, x yy zx z

    Alias of the forward direction of ZFSet.isTransitive_iff_mem_trans.