English
A PredOrder α can be built from a linear order α with a pred, together with proofs that pred relates to < and ≤ in a coherent way; this defines pred, pred_le, and min_of_le_pred.
Русский
PredOrder α строится из линейного порядка α с предикатом pred и доказательствами согласованности, задающими pred, pred_le и min_of_le_pred.
LaTeX
$$$\\text{PredOrder}(\\alpha) = \\{ pred,\\ pred\\le,\\ pred\\le\\_, \\text{мин}\_\\text{of}\\_\\text{le_pred} \\}$ (конструктивная запись).$$
Lean4
/-- A constructor for `PredOrder α` for `α` a linear order. -/
@[simps]
def ofCore (pred : α → α) (hn : ∀ {a}, ¬IsMin a → ∀ b, b ≤ pred a ↔ b < a) (hm : ∀ a, IsMin a → pred a = a) :
PredOrder α :=
{ pred
le_pred_of_lt := fun {a b} => by_cases (fun h hab => (hm b h).symm ▸ hab.le) fun h => (hn h a).mpr
pred_le := fun a => by_cases (fun h => (hm a h).le) fun h => le_of_lt <| by simpa using (hn h a).not
min_of_le_pred := fun {a} => not_imp_not.mp fun h => by simpa using (hn h a).not }
