toTopHom

Mathlib.Order.Hom.Bounded

URI: https://scilib.ai/kg/mathlib#BoundedOrderHom.toTopHom

English

Injectivity of the underlying function map: the map f ↦ f.toFun is injective on BotHom.

Русский

Инъективность отображения подлежащей функции: f ↦ f.toFun инъективно на BotHom.

LaTeX

$$∃! f,g: BotHom α β, f.toFun = g.toFun ⇒ f=g.$$

Lean4

/-- Reinterpret a `BoundedOrderHom` as a `TopHom`. -/
def toTopHom (f : BoundedOrderHom α β) : TopHom α β :=
  { f with }

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

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

Разделы

Аффилиация

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