mem_of_append

Mathlib.SetTheory.Descriptive.Tree

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

← MathLib Explorer

English

If x ++ y ∈ T, then x ∈ T for a tree T on A.

Русский

Если x ++ y принадлежит дереву T над A, то x принадлежит T.

LaTeX

$$$ \\forall x,y:\\mathrm{List}(A),\\; (x\\!+\\!+y) \\in T \\Rightarrow x \\in T $$$

Lean4

theorem mem_of_append {x y : List A} (h : x ++ y ∈ T) : x ∈ T := by
  induction y generalizing x with
  | nil => simpa using h
  | cons y ys ih => exact T.prop (ih (by simpa))

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

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

Разделы

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

Аффилиация

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