out_eq'

Mathlib.Data.Quot

URI: https://scilib.ai/kg/mathlib#Quotient.out_eq'

English

For any q in Quotient s1, mk''(q.out) equals q.

Русский

Для любого q в Quotient s1, mk''(q.out) равно q.

LaTeX

$$$\\forall q:\\, \\operatorname{Quotient}(s_1),\\ \\operatorname{Quotient.mk''}(q^{\\mathrm{out}}) = q$$$

Lean4

theorem out_eq' (q : Quotient s₁) : Quotient.mk'' q.out = q :=
  q.out_eq

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

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

Разделы

Аффилиация

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