map_id

Mathlib.Computability.RegularExpressions

URI: https://scilib.ai/kg/mathlib#RegularExpression.map_id

Lean4

@[simp]
theorem map_id : ∀ P : RegularExpression α, P.map id = P
  | 0 => rfl
  | 1 => rfl
  | char _ => rfl
  | R + S => by simp_rw [map, map_id]
  | R * S => by simp_rw [map, map_id]
  | star R => by simp_rw [map, map_id]

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

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

Разделы

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

Аффилиация

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