sound' — Mathlib

English

If a is related to b in the setoid, then mk'' a and mk'' b are equal in the quotient.

Русский

Если a эквивалентен b по множеству эквивалентностей, то mk'' a = mk'' b в фактор-множстве.

LaTeX

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

Lean4

theorem sound' {a b : α} : s₁ a b → @Quotient.mk'' α s₁ a = Quotient.mk'' b :=
  Quotient.sound

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