liftOn

Mathlib.Data.Finmap

URI: https://scilib.ai/kg/mathlib#Finmap.liftOn

Lean4

/-- Lift a permutation-respecting function on `AList` to `Finmap`. -/
def liftOn {γ} (s : Finmap β) (f : AList β → γ) (H : ∀ a b : AList β, a.entries ~ b.entries → f a = f b) : γ :=
  by
  refine
    (Quotient.liftOn s.entries (fun (l : List (Sigma β)) => (⟨_, fun nd => f ⟨l, nd⟩⟩ : Part γ))
            (fun l₁ l₂ p => Part.ext' (perm_nodupKeys p) ?_) :
          Part γ).get
      ?_
  · exact fun h1 h2 => H _ _ p
  · have := s.nodupKeys
    revert this
    rcases s.entries with ⟨l⟩
    exact id

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

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

Разделы

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

Аффилиация

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