coe_fn_injective

Mathlib.Order.RelIso.Basic

URI: https://scilib.ai/kg/mathlib#RelHom.coe_fn_injective

← MathLib Explorer

English

Two RelHom are equal if they agree on all inputs.

Русский

Два RelHom равны, если совпадают на всех аргументах.

LaTeX

$$$\forall \{f\ g : r \to r\, s\},\ (\forall x, f x = g x) \Rightarrow f = g$$$

Lean4

/-- The map `coe_fn : (r →r s) → (α → β)` is injective. -/
theorem coe_fn_injective : Injective fun (f : r →r s) => (f : α → β) :=
  DFunLike.coe_injective

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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