eq' — Mathlib

English

Equality of mk' representations is equivalent to the setoid relation.

Русский

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

LaTeX

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

Lean4

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

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