ofLePredIff — Mathlib

English

A PredOrder structure on α from a predicate pred with the equivalence a ≤ pred b ⇔ a < b.

Русский

PredOrder α строится из pred при условии эквивалентности a ≤ pred b ⇔ a < b.

LaTeX

$$$\\text{PredOrder}(\\alpha) = \\{ pred,\\ (a \\le pred b) \\iff (a < b) \\}$.$$

Lean4

/-- A constructor for `PredOrder α` usable when `α` has no minimal element. -/
def ofLePredIff (pred : α → α) (hle_pred_iff : ∀ {a b}, a ≤ pred b ↔ a < b) : PredOrder α :=
  { pred
    pred_le := fun _ => (hle_pred_iff.1 le_rfl).le
    min_of_le_pred := fun ha => (lt_irrefl _ <| hle_pred_iff.1 ha).elim
    le_pred_of_lt := fun h => hle_pred_iff.2 h }

Похожие утверждения