Commit 2026-04-14 15:28 e76c1b32

feat(Order/Partition): every partition has IsRepFun (#36691) This PR expands the API for Setoid.Partition (or Partition) by introducing definitions and lemmas for working with representatives and specific parts of a partition.

Key Additions

• Partition.rep: Noncomputably chooses a representative from a given part of a partition, along with basic membership lemmas (rep_mem, rep_mem').
• Partition.partOf: Defines the part of a partition containing a specific element (evaluates to ∅ if the element is not in the underlying set).
• IsRepFun extensions:
  • exists_extend_partial / exists_extend_partial': Proves that partially defined representative functions can be extended to complete ones.
  • nonempty: Proves that every partition admits at least one representative function.