Commit 2022-12-13 21:37 84da13bd

View on Github →

feat: port Data.Set.Opposite (#983) Mathlib SHA: fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e The file produced by mathport had 0 errors! (And all proofs have become by rfl!)

Estimated changes

added theorem Set.mem_op
added theorem Set.mem_unop
added def Set.opEquiv
added def Set.opEquiv_self
added theorem Set.op_mem_op
added theorem Set.op_unop
added theorem Set.singleton_op
added theorem Set.singleton_op_unop
added theorem Set.singleton_unop
added theorem Set.singleton_unop_op
added theorem Set.unop_mem_unop
added theorem Set.unop_op