id_map

Mathlib.Data.Tree.Basic

URI: https://scilib.ai/kg/mathlib#Tree.id_map

English

Applying the identity to every node leaves the tree unchanged.

Русский

Применение тождественной функции ко всем узлам оставляет дерево без изменений.

LaTeX

$$$ t.map(\mathrm{id}) = t $$$

Lean4

theorem id_map (t : Tree α) : t.map id = t := by
  induction t with
  | nil => rw [map]
  | node v l r hl hr => rw [map, hl, hr, id_eq]

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

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

Разделы

Аффилиация

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