Commit 2024-10-31 09:16 7c7a48f0

View on Github →

chore(Order/InitialSeg): private / delete inner workings (#17609) This PR does the following:

private and rename Antisymm.aux.
private and golf collapseF, collapseF.lt, and collapseF.not_lt.
golf collapse and improve the docstring.
delete collapse_apply which no longer makes much sense to have.

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

deleted theorem InitialSeg.Antisymm.aux

deleted theorem RelEmbedding.collapseF.lt

deleted theorem RelEmbedding.collapseF.not_lt

deleted theorem RelEmbedding.collapse_apply

Modified Mathlib/Order/RelClasses.lean

modified theorem trans_trichotomous_left

modified theorem trans_trichotomous_right