mk_eq_iff_out

Mathlib.Data.Quot

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

← MathLib Explorer

English

For any s, x, y, the equality ⟦x⟧ = y holds iff x ≈ Quotient.out y.

Русский

Для любых x и y верно: ⟦x⟧ = y ⇔ x ≈ Quotient.out y.

LaTeX

$$$\\overline{x} = y \\iff x \\approx \\mathrm{out}(y)$$$

Lean4

theorem mk_eq_iff_out {s : Setoid α} {x : α} {y : Quotient s} : ⟦x⟧ = y ↔ x ≈ Quotient.out y :=
  by
  refine Iff.trans ?_ Quotient.eq
  rw [Quotient.out_eq y]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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