eqToHom' — Mathlib

English

For any a, b in α and equality h: a = b, there is a morphism from Discrete.mk a to Discrete.mk b, obtained from equality.

Русский

Для любых a, b в α и равенства h: a = b существует морфизм Discrete.mk a ⟶ Discrete.mk b, полученный из равенства.

LaTeX

$$$\\exists h:\\ a=b \\;\\Rightarrow\\; \\mathrm{Hom}_{\\mathrm{Discrete}(\\alpha)}(\\mathrm{mk}(a),\\mathrm{mk}(b))$ содержит элемент, соответствующий $h$$$

Lean4

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

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