eq_mk_iff_out

Mathlib.Data.Quot

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

← MathLib Explorer

English

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

Русский

Для любых x, y ∈ α: x = ⟦y⟧ эквивалентно Quotient.out x ≈ y.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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