eqToIso' — Mathlib

English

If a = b for elements a,b in α, there is an isomorphism Discrete.mk a ≅ Discrete.mk b, given by equality.

Русский

Если a = b для элементов α, существует изоморфизм Discrete.mk a ≅ Discrete.mk b, задаваемый равенством.

LaTeX

$$$\\mathrm{eqToIso}(h): \\mathrm{Discrete.mk}(a) \\cong \\mathrm{Discrete.mk}(b) \\quad( h: a=b )$$$

Lean4

/-- A variant of `eqToIso` that lifts terms to the discrete category. -/
abbrev eqToIso' {a b : α} (h : a = b) : Discrete.mk a ≅ Discrete.mk b :=
  Discrete.eqToIso h

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