toSetoid_inj — Mathlib

English

The map sending a congruence to its underlying Setoid is injective: if c.toSetoid = d.toSetoid then c = d.

Русский

Отображение конгруэнции к её базовой Setoid инъективно: если c.toSetoid = d.toSetoid, то c = d.

LaTeX

$$$c.toSetoid = d.toSetoid \\Rightarrow c = d$$$

Lean4

/-- The map sending a congruence relation to its underlying equivalence relation is injective. -/
@[to_additive /-- The map sending an additive congruence relation to its underlying equivalence
    relation is injective. -/
    ]
theorem toSetoid_inj {c d : Con M} (H : c.toSetoid = d.toSetoid) : c = d :=
  ext <| Setoid.ext_iff.1 H

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