lt_iff_cons_le — Mathlib

English

A multiset s is strictly less than t iff there exists an element whose insertion into s is below t.

Русский

Мультимножество s строго меньше t тогда и только тогда, когда существует элемент, вставка которого в s лежит ниже t.

LaTeX

$$s < t \iff \exists a, insert(a,s) \le t$$

Lean4

theorem lt_iff_cons_le {s t : Multiset α} : s < t ↔ ∃ a, a ::ₘ s ≤ t :=
  ⟨Quotient.inductionOn₂ s t fun _l₁ _l₂ h => Subperm.exists_of_length_lt (le_of_lt h) (card_lt_card h), fun ⟨_a, h⟩ =>
    lt_of_lt_of_le (lt_cons_self _ _) h⟩

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