Commit 2025-02-18 09:18 2836c275

View on Github →

chore: move some results from Order.RelClasses earlier (#21144)

Estimated changes

Modified Mathlib/Data/Sigma/Lex.lean

Modified Mathlib/Order/Defs/Unbundled.lean

added theorem antisymm'

added theorem antisymm_iff

added theorem antisymm_of'

added theorem antisymm_of

added theorem comm

added theorem comm_of

added theorem empty_relation_apply

added theorem extensional_of_trichotomous_of_irrefl

added theorem ne_of_irrefl'

added theorem ne_of_irrefl

added theorem not_rel_of_subsingleton

added theorem of_eq

added theorem rel_congr

added theorem rel_congr_left

added theorem rel_congr_right

added theorem rel_of_subsingleton

added theorem trans_trichotomous_left

added theorem trans_trichotomous_right

added theorem transitive_of_trans

Modified Mathlib/Order/RelClasses.lean

deleted theorem antisymm'

deleted theorem antisymm_iff

deleted theorem antisymm_of'

deleted theorem antisymm_of

deleted theorem comm

deleted theorem comm_of

deleted theorem empty_relation_apply

deleted theorem extensional_of_trichotomous_of_irrefl

deleted theorem ne_of_irrefl'

deleted theorem ne_of_irrefl

deleted theorem not_rel_of_subsingleton

deleted theorem of_eq

deleted theorem rel_congr

deleted theorem rel_congr_left

deleted theorem rel_congr_right

deleted theorem rel_of_subsingleton

deleted theorem trans_trichotomous_left

deleted theorem trans_trichotomous_right

deleted theorem transitive_of_trans