eqvGen_exact — Mathlib

English

If two representatives are equal in the quotient by r, then they are equivalent under EqvGen r.

Русский

Если два элемента идентичны в результате факторинга по r, то они эквивалентны по EqvGen r.

LaTeX

$$$\\\\forall a b, \\\\quot mk r a = \\\\quot mk r b \\\\Rightarrow \\\\operatorname{EqvGen} r a b$$$

Lean4

theorem eqvGen_exact (H : Quot.mk r a = Quot.mk r b) : EqvGen r a b :=
  @Quotient.exact _ (EqvGen.setoid r) a b
    (congrArg (Quot.lift (Quotient.mk (EqvGen.setoid r)) (fun x y h ↦ Quot.sound (EqvGen.rel x y h))) H)

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