exists_cons_of_mem — Mathlib

English

If s ∈ Sym α (n+1) and a ∈ s, then there exists t with s = a ::ₛ t and card(t) = n.

Русский

Если s ∈ Sym α (n+1) и a ∈ s, то существует t такое, что s = a ::ₛ t и card(t) = n.

LaTeX

$$$ \exists t, s = a ::ₛ t \text{ and } \operatorname{card}(t) = n. $$$

Lean4

theorem exists_cons_of_mem {s : Sym α (n + 1)} {a : α} (h : a ∈ s) : ∃ t, s = a ::ₛ t :=
  by
  obtain ⟨m, h⟩ := Multiset.exists_cons_of_mem h
  have : Multiset.card m = n := by
    apply_fun Multiset.card at h
    rw [s.2, Multiset.card_cons, add_left_inj] at h
    exact h.symm
  use ⟨m, this⟩
  apply Subtype.ext
  exact h

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