out_eq

Mathlib.Data.Quot

URI: https://scilib.ai/kg/mathlib#Quot.out_eq

English

For any q in Quot r, Quot.mk r (q.out) equals q.

Русский

Для любого q в Quot r, Quot.mk r (q.out) равно q.

LaTeX

$$$\\mathrm{Quot.mk} r (q^{\\mathrm{out}}) = q$$$

Lean4

@[simp]
theorem out_eq {r : α → α → Prop} (q : Quot r) : Quot.mk r q.out = q :=
  Classical.choose_spec (Quot.exists_rep q)

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

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

Разделы

Аффилиация

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