Commit 2025-03-11 10:33 95761505

View on Github →

chore(Data/Set): some more porting notes (#22800) This builds on #22765 and gets rid of a few more porting notes.

Estimated changes

modified theorem Set.surjOn_id
modified theorem Set.up_empty
modified theorem Set.up_mul
modified theorem Set.up_one
modified theorem Set.up_union
modified theorem SetSemiring.add_def
modified theorem SetSemiring.down_add
modified theorem SetSemiring.down_mul
modified theorem SetSemiring.down_one
modified theorem SetSemiring.down_zero
modified theorem SetSemiring.mul_def
modified theorem SetSemiring.up_le_up
modified theorem SetSemiring.up_lt_up