class Std.Internal.IsCut {α : Type u} (cmp : α → α → Ordering) (cut : α → Ordering) : Prop

• lt {k k' : α} : cut k' = Ordering.lt → cmp k' k = Ordering.lt → cut k = Ordering.lt
• gt {k k' : α} : cut k' = Ordering.gt → cmp k' k = Ordering.gt → cut k = Ordering.gt

class Std.Internal.IsStrictCut {α : Type u} (cmp : α → α → Ordering) (cut : α → Ordering) extends Std.Internal.IsCut cmp cut : Prop

• lt {k k' : α} : cut k' = Ordering.lt → cmp k' k = Ordering.lt → cut k = Ordering.lt
• gt {k k' : α} : cut k' = Ordering.gt → cmp k' k = Ordering.gt → cut k = Ordering.gt
• eq (k : α) {k' : α} : cut k' = Ordering.eq → cut k = cmp k' k

theorem Std.Internal.IsStrictCut.gt_of_isGE_of_gt {α : Type u} {cmp : α → α → Ordering} {cut : α → Ordering} [IsStrictCut cmp cut] {k k' : α} : (cut k').isGE = true → cmp k' k = Ordering.gt → cut k = Ordering.gt

theorem Std.Internal.IsStrictCut.lt_of_isLE_of_lt {α : Type u} {cmp : α → α → Ordering} {cut : α → Ordering} [IsStrictCut cmp cut] {k k' : α} : (cut k').isLE = true → cmp k' k = Ordering.lt → cut k = Ordering.lt