mathlib
730c6d4c - chore(order/initial_seg): tweak `subsingleton_of_trichotomous_of_irrefl` (#18749)

Commit

2 years ago

chore(order/initial_seg): tweak `subsingleton_of_trichotomous_of_irrefl` (#18749) We rename it, turn it into an instance, and golf the next instance with it.

Author

vihdzp

Parents

17219820

mathlib 730c6d4c - chore(order/initial_seg): tweak `subsingleton_of_trichotomous_of_irrefl` (#18749)

mathlib
730c6d4c - chore(order/initial_seg): tweak `subsingleton_of_trichotomous_of_irrefl` (#18749)