eq''

Mathlib.Data.Quot

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

English

Equality of mk'' a and mk'' b is equivalent to the setoid relation.

Русский

Равенство mk'' a и mk'' b эквивалентно отношению по множеству эквивалентности.

LaTeX

$$$\\forall a,b:\\, s_1 a b \\iff \\operatorname{Quotient.mk''} a = \\operatorname{Quotient.mk''} b$$$

Lean4

protected theorem eq'' {a b : α} : @Quotient.mk'' α s₁ a = Quotient.mk'' b ↔ s₁ a b :=
  Quotient.eq

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

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

Разделы

Аффилиация

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