- 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
Instances
class
Std.Internal.IsStrictCut
{α : Type u}
(cmp : α → α → Ordering)
(cut : α → Ordering)
extends Std.Internal.IsCut cmp cut :
Instances
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
instance
Std.Internal.instIsStrictCutCompareLt
{α : Type u}
[Ord α]
:
IsStrictCut compare fun (x : α) => Ordering.lt
instance
Std.Internal.instIsStrictCutCompareThenGt
{α : Type u}
[Ord α]
[TransOrd α]
{k : α}
:
IsStrictCut compare fun (k' : α) => (compare k k').then Ordering.gt