addGCongrLemmaEntry

Mathlib.Tactic.GCongr.Core

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.GCongr.addGCongrLemmaEntry

Lean4

/-- Insert a `GCongrLemma` in a collection of lemmas, making sure that the lemmas are sorted. -/
def addGCongrLemmaEntry (m : GCongrLemmas) (l : GCongrLemma) : GCongrLemmas :=
  match m[l.key]? with
  | none => m.insert l.key [l]
  | some es => m.insert l.key <| insert l es
where/-- - Insert a `GCongrLemma` in the correct place in a list of lemmas. -/
   insert (l : GCongrLemma) : List GCongrLemma → List GCongrLemma
    | [] => [l]
    | l' :: ls => if l'.prioLE l then l :: l' :: ls else l' :: insert l ls

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

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

Разделы

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

Аффилиация

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