encodableQuotient

Mathlib.Logic.Encodable.Basic

URI: https://scilib.ai/kg/mathlib#encodableQuotient

Lean4

/-- The quotient of an encodable space by a decidable equivalence relation is encodable. -/
def encodableQuotient : Encodable (Quotient s) :=
  ⟨fun q => encode q.rep, fun n => Quotient.mk'' <$> decode n, by rintro ⟨l⟩; dsimp; rw [encodek];
    exact congr_arg some ⟦l⟧.rep_spec⟩

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

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

Разделы

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

Аффилиация

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