le_iff_exists_add — Mathlib

English

For multisets s, t: s ≤ t iff ∃ u with t = s + u.

Русский

Для мультисетов s и t: s ⊆ t тогда и только тогда, когда существует u such that t = s + u.

LaTeX

$$$s \le t \iff \exists u, t = s + u$$$

Lean4

theorem le_iff_exists_add {s t : Multiset α} : s ≤ t ↔ ∃ u, t = s + u :=
  ⟨fun h =>
    leInductionOn h fun s =>
      let ⟨l, p⟩ := s.exists_perm_append
      ⟨l, Quot.sound p⟩,
    fun ⟨_u, e⟩ => e.symm ▸ le_add_right _ _⟩

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