exact' — Mathlib

English

If the quotient constructors of a and b are equal, then a and b are related by the setoid.

Русский

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

LaTeX

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

Lean4

theorem exact' {a b : α} : (Quotient.mk'' a : Quotient s₁) = Quotient.mk'' b → s₁ a b :=
  Quotient.exact

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