instExistsAddOfLE — Mathlib

English

If s ≤ t for multisets, then there exists a multiset l such that t = s + l (i.e., t is obtained by adding some multiset to s).

Русский

Если s ≤ t для мультимножеств, тогда существует такое l, что t = s + l (t получается добавлением некоторого мультимножества к s).

LaTeX

$$$s \le t \Rightarrow \exists l\ (t = s + l).$$$

Lean4

instance : ExistsAddOfLE (Multiset α) where
  exists_add_of_le
    h :=
    leInductionOn h fun s ↦
      let ⟨l, p⟩ := s.exists_perm_append;
      ⟨l, Quot.sound p⟩

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