eval

Mathlib.Data.Quot

URI: https://scilib.ai/kg/mathlib#Quotient.eval

Lean4

/-- Given a class of functions `q : @Quotient (∀ i, α i) _`, returns the class of `i`-th projection
`Quotient (S i)`. -/
def eval {ι : Type*} {α : ι → Sort*} {S : ∀ i, Setoid (α i)} (q : @Quotient (∀ i, α i) (by infer_instance)) (i : ι) :
    Quotient (S i) :=
  q.map (· i) fun _ _ h ↦ by exact h i

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

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

Разделы

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

Аффилиация

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