IsDershowitzMannaLT — Mathlib

English

For any α, r, and l, Multiset.Pairwise r (Multiset.ofList l) holds iff there exists l' with l ~ l' and l'.Pairwise r.

Русский

Для любого α, r и l, Multiset.Pairwise r (Multiset.ofList l) эквивалентно существованию l' такое, что l ~ l' и l'.Pairwise r.

LaTeX

$$$\\forall \\alpha\\,\\forall r:\\alpha\\to\\alpha\\to\\mathrm{Prop}\\,\\forall l:\\mathrm{List}(\\alpha),\\ \\text{Multiset.Pairwise } r(\\text{Multiset.ofList } l)\\iff \\exists l'\\; l\\sim l'\\wedge l'.\\text{Pairwise } r$$$

Lean4

/-- The standard Dershowitz–Manna ordering. -/
def IsDershowitzMannaLT (M N : Multiset α) : Prop :=
  ∃ X Y Z, Z ≠ ∅ ∧ M = X + Y ∧ N = X + Z ∧ ∀ y ∈ Y, ∃ z ∈ Z, y < z

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