singleton_mem

Mathlib.SetTheory.Descriptive.Tree

URI: https://scilib.ai/kg/mathlib#Descriptive.Tree.singleton_mem

English

If a ∈ T for a tree T and an element x, then the singleton [a] ∈ T.

Русский

Если a ∈ T, тогда конструктор-одиночный элемент [a] ∈ T.

LaTeX

$$$ a \\in T \\Rightarrow [a] \\in T $$$

Lean4

theorem singleton_mem (T : tree A) {a : A} {x : List A} (h : a :: x ∈ T) : [a] ∈ T :=
  mem_of_prefix ⟨x, rfl⟩ h

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

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

Разделы

Аффилиация

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