coe_inj

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.ContinuousHom.coe_inj

English

If two continuous homomorphisms have the same underlying function, they are equal.

Русский

Если два непрерывных гомоморфизма имеют одинаковую базовую функцию, они равны.

LaTeX

$$$ (f,g:\mathrm{ContinuousHom}(\alpha,\beta))\ ((f:\alpha\to\beta)=g)\Rightarrow f=g$$$

Lean4

protected theorem coe_inj (f g : α →𝒄 β) (h : (f : α → β) = g) : f = g :=
  DFunLike.ext' h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru