Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-04 18:40 7ec5e87f

View on Github →

feat(set_theory/lists): finite ZFA

Estimated changes

added def finsets
added def lists'.cons
added theorem lists'.cons_subset
added theorem lists'.mem_cons
added theorem lists'.mem_def
added theorem lists'.mem_equiv_left
added theorem lists'.mem_of_subset'
added theorem lists'.mem_of_subset
added def lists'.of_list
added theorem lists'.of_list_subset
added theorem lists'.of_to_list
added theorem lists'.subset.refl
added theorem lists'.subset.trans
added theorem lists'.subset_def
added theorem lists'.subset_nil
added def lists'.to_list
added theorem lists'.to_list_cons
added theorem lists'.to_of_list
added def lists.atom
added theorem lists.equiv.symm
added theorem lists.equiv.trans
added theorem lists.equiv_atom
added def lists.is_list
added theorem lists.is_list_of_mem
added theorem lists.is_list_to_list
added theorem lists.lt_sizeof_cons'
added def lists.mem
added def lists.of'
added def lists.of_list
added theorem lists.of_to_list
added theorem lists.sizeof_pos
added def lists.to_list
added theorem lists.to_of_list
added def lists
added inductive {u}