Commit 2026-02-06 11:53 d50d677c

View on Github →

chore(Order/Defs/Unbundled): deprecate IsTrichotomous in favor of core's Std.Trichotomous (#34349)

Estimated changes

modified theorem trans_trichotomous_left
modified theorem trans_trichotomous_right
modified theorem trichotomous
modified theorem trichotomous_of
modified theorem PrincipalSeg.ext
deleted theorem Pi.isTrichotomous_lex
added theorem Pi.trichotomous_lex
modified theorem isChain_of_trichotomous
modified theorem isChain_univ_iff
deleted theorem InvImage.isTrichotomous
added theorem InvImage.trichotomous
deleted theorem IsTrichotomous.swap
added theorem Std.Trichotomous.swap
modified theorem RelEmbedding.ofMonotone_coe
modified theorem injective_of_increasing