root_ne_bot_of_mem_subtrees

Mathlib.Order.SuccPred.Tree

URI: https://scilib.ai/kg/mathlib#SubRootedTree.root_ne_bot_of_mem_subtrees

← MathLib Explorer

English

Every subtree rooted at an atom has a non-bottom root.

Русский

Каждое поддерево с корнем в атоме имеет корень, не равный ⊥.

LaTeX

$$∀ r ∈ t.subtrees, r.root ≠ ⊥$$

Lean4

theorem root_ne_bot_of_mem_subtrees (r : SubRootedTree t) (hr : r ∈ t.subtrees) : r.root ≠ ⊥ :=
  by
  simp only [RootedTree.subtrees, Set.mem_setOf_eq] at hr
  exact hr.1

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

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

Разделы

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

Аффилиация

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