Commit 2023-03-24 18:51 6f748f1a

View on Github →

feat: port Data.Finset.Sym (#2168) Some instances that were not synthezised automatically are added to the files Data.Sym.Basic and Data.Sym.Sym2 See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Classical

Estimated changes

added theorem Finset.mem_sym2_iff
added theorem Finset.mem_sym_iff
added theorem Finset.sym2_empty
added theorem Finset.sym2_eq_empty
added theorem Finset.sym2_mono
added theorem Finset.sym2_nonempty
added theorem Finset.sym2_singleton
added theorem Finset.sym2_univ
added theorem Finset.sym_empty
added theorem Finset.sym_eq_empty
added theorem Finset.sym_fill_mem
added theorem Finset.sym_inter
added theorem Finset.sym_mono
added theorem Finset.sym_nonempty
added theorem Finset.sym_singleton
added theorem Finset.sym_succ
added theorem Finset.sym_union
added theorem Finset.sym_univ
added theorem Finset.sym_zero