equal
deleted
inserted
replaced
76 asymp_on_conversep[simp] |
76 asymp_on_conversep[simp] |
77 irreflD |
77 irreflD |
78 irrefl_onD |
78 irrefl_onD |
79 irrefl_onI |
79 irrefl_onI |
80 irrefl_on_converse[simp] |
80 irrefl_on_converse[simp] |
|
81 irrefl_on_if_asym_on[simp] |
81 irrefl_on_subset |
82 irrefl_on_subset |
82 irreflpD |
83 irreflpD |
83 irreflp_onD |
84 irreflp_onD |
84 irreflp_onI |
85 irreflp_onI |
85 irreflp_on_converse[simp] |
86 irreflp_on_converse[simp] |
|
87 irreflp_on_if_asymp_on[simp] |
86 irreflp_on_irrefl_on_eq[pred_set_conv] |
88 irreflp_on_irrefl_on_eq[pred_set_conv] |
87 irreflp_on_subset |
89 irreflp_on_subset |
88 linorder.totalp_on_ge[simp] |
90 linorder.totalp_on_ge[simp] |
89 linorder.totalp_on_greater[simp] |
91 linorder.totalp_on_greater[simp] |
90 linorder.totalp_on_le[simp] |
92 linorder.totalp_on_le[simp] |