mk_out'

Mathlib.Data.Quot

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

English

For any a in α, the relation s1 holds between the quotient mk'' a and its out value.

Русский

Для любого a ∈ α отношение s1 держится между mk'' a и его значением out.

LaTeX

$$$s_1( (\\operatorname{Quotient.mk''} a : \\operatorname{Quotient}(s_1)).\\mathrm{out}, a )$$$

Lean4

theorem mk_out' (a : α) : s₁ (Quotient.mk'' a : Quotient s₁).out a :=
  Quotient.exact (Quotient.out_eq _)

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

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

Разделы

Аффилиация

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