exists_eq_cons_of_succ

Mathlib.Data.Sym.Basic

URI: https://scilib.ai/kg/mathlib#Sym.exists_eq_cons_of_succ

← MathLib Explorer

English

For s ∈ Sym α (n+1), there exists a and s' with s = a ::ₛ s'.

Русский

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

LaTeX

$$$ \exists a \; \exists s' , s = a ::ₛ s'. $$$

Lean4

theorem exists_eq_cons_of_succ (s : Sym α n.succ) : ∃ (a : α) (s' : Sym α n), s = a ::ₛ s' :=
  by
  obtain ⟨a, ha⟩ := exists_mem s
  classical exact ⟨a, s.erase a ha, (cons_erase ha).symm⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru