mk_out

Mathlib.Data.Quot

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

English

For any a, s ((⟦a⟧).out) a holds: the out of the class representative relates back to a.

Русский

Для любого a верно: s( (⟦a⟧).out, a ), то есть representing a и его out возвращаются обратно к a.

LaTeX

$$$s\\bigl((\\overline{a})^{\\mathrm{out}}, a\\bigr)$$$

Lean4

theorem mk_out {s : Setoid α} (a : α) : s (⟦a⟧ : Quotient s).out a :=
  Quotient.exact (Quotient.out_eq _)

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

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

Разделы

Аффилиация

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