Commit 2024-09-14 05:31 b95daa50

View on Github →

chore: tidy/move/deprecate Init.Logic and IsSymmOp more (#16757)

  • Move EmptyRelation to Order.Defs (and use Type*, Sort* throughout the latter file while I'm at it).
  • Deprecate the two InvImage theorems and three Equivalence theorems in Init.Logic and fix the few uses of them.
  • Align IsSymmOp with the new typeclasses of #16751, i.e. make its α and β arguments implicit. There were a number of uses of IsSymmOp where Std.Commutative could also be used; make those changes.

Estimated changes

modified theorem contravariant_flip_iff
modified theorem covariant_flip_iff
added theorem IsSymmOp.flip_eq
deleted def EmptyRelation
modified theorem Equivalence.reflexive
modified theorem Equivalence.symmetric
modified theorem Equivalence.transitive
deleted theorem IsSymmOp.flip_eq
added def EmptyRelation
modified def maxDefault
modified def minDefault