Commit 2024-09-16 02:13 14a4ecec

View on Github →

chore: final cleanup of Mathlib.Init (#16796)

  • Move the trans attributes on Iff and HEq in Init.Logic to Logic.Basic.
  • Move the six undeprecated relation definitions in the same file to Order.Defs.
  • Remove the refl attribute on Iff.refl – it has been upstreamed in leanprover/lean4#5329. This concludes the cleanup of Mathlib.Init.

Estimated changes

deleted def AntiSymmetric
deleted theorem Equivalence.reflexive
deleted theorem Equivalence.symmetric
deleted theorem Equivalence.transitive
deleted theorem InvImage.irreflexive
deleted theorem InvImage.trans
deleted def Irreflexive
deleted def Reflexive
deleted def Symmetric
deleted def Total
deleted def Transitive
added def AntiSymmetric
added theorem Equivalence.reflexive
added theorem Equivalence.symmetric
added theorem Equivalence.transitive
added theorem InvImage.irreflexive
added theorem InvImage.trans
added def Irreflexive
added def Reflexive
added def Symmetric
added def Total
added def Transitive