lt_cons_self — Mathlib

English

For any multiset s and element a, the multiset obtained by inserting a at the front is strictly larger than s.

Русский

Для любого мультимножества s и элемента a мультимножество, полученное добавлением a в начало, строго больше чем s.

LaTeX

$$$s < a \operatorname{insert} s$$$

Lean4

theorem lt_cons_self (s : Multiset α) (a : α) : s < a ::ₘ s :=
  Quot.inductionOn s fun l =>
    suffices l <+~ a :: l ∧ ¬l ~ a :: l by simpa [lt_iff_le_and_ne]
    ⟨(sublist_cons_self _ _).subperm, fun p => _root_.ne_of_lt (lt_succ_self (length l)) p.length_eq⟩

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