Commit 2023-02-02 19:31 251eade7

View on Github →

feat: port SetTheory.Lists (#1575)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Lists.lean

added def Finsets

added theorem Lists'.Subset.refl

added theorem Lists'.Subset.trans

added inductive Lists'.Subset

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'.ofList

added theorem Lists'.ofList_subset

added theorem Lists'.of_toList

added theorem Lists'.subset_def

added theorem Lists'.subset_nil

added def Lists'.toList

added theorem Lists'.toList_cons

added theorem Lists'.to_ofList

added inductive Lists'.{u}

added theorem Lists.Equiv.antisymm_iff

added theorem Lists.Equiv.symm

added theorem Lists.Equiv.trans

added inductive Lists.Equiv

added def Lists.IsList

added def Lists.atom

added theorem Lists.equiv_atom

added theorem Lists.isList_toList

added theorem Lists.is_list_of_mem

added theorem Lists.lt_sizeof_cons'

added def Lists.mem

added def Lists.of'

added def Lists.ofList

added theorem Lists.of_toList

added theorem Lists.sizeof_pos

added def Lists.toList

added theorem Lists.to_ofList

added def Lists