ofLeftInverse

Mathlib.Logic.Encodable.Basic

URI: https://scilib.ai/kg/mathlib#Encodable.ofLeftInverse

Lean4

/-- If `α` is encodable and `f : β → α` is invertible, then `β` is encodable as well. -/
def ofLeftInverse [Encodable α] (f : β → α) (finv : α → β) (linv : ∀ b, finv (f b) = b) : Encodable β :=
  ofLeftInjection f (some ∘ finv) fun b => congr_arg some (linv b)

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

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

Разделы

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

Аффилиация

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