mem_of_prefix

Mathlib.SetTheory.Descriptive.Tree

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

English

If x is a prefix of y and y ∈ T, then x ∈ T.

Русский

Если x является префиксом y и y ∈ T, то x ∈ T.

LaTeX

$$$ x \\sqsubseteq y \\Rightarrow y \\in T \\Rightarrow x \\in T $$$

Lean4

theorem mem_of_prefix {x y : List A} (h' : x <+: y) (h : y ∈ T) : x ∈ T := by obtain ⟨_, rfl⟩ := h';
  exact mem_of_append h

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

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

Разделы

Аффилиация

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