eq_iff_equiv

Mathlib.Data.Quot

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

English

For any Setoid α, and x,y ∈ α, Quot.mk r x = ⟦y⟧ holds if and only if x ≈ y.

Русский

Для множества эквивалентности α и элементов x,y: Quot.mk r x = ⟦y⟧ тогда и только тогда, когда x ≈ y.

LaTeX

$$$\\Quotient.mk r x = \\overline{y} \\;\\iff\\; x \\approx y$$$

Lean4

theorem eq_iff_equiv {r : Setoid α} {x y : α} : Quotient.mk r x = ⟦y⟧ ↔ x ≈ y :=
  Quotient.eq

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

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

Разделы

Аффилиация

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