exists_rep

Mathlib.Data.Quot

URI: https://scilib.ai/kg/mathlib#Trunc.exists_rep

English

Every truncated element q has a representative a in α such that mk'' a = q.

Русский

Каждый усечённый элемент q имеет представителя a в α, такой что mk'' a = q.

LaTeX

$$$\\exists a:\\, \\alpha,\\ mk'' a = q$$$

Lean4

theorem exists_rep (q : Trunc α) : ∃ a : α, mk a = q :=
  Quot.exists_rep q

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

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

Разделы

Аффилиация

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