coe_fn_injective — Mathlib

English

The map taking a RelIso to its underlying function is injective: if two RelIso's have the same underlying function, they are equal.

Русский

Отображение, которое сопоставляет RelIso его базовой функции, инъективно: если два RelIso имеют одну и ту же базовую функцию, они равны.

LaTeX

$$$\text{Injective }(\lambda f:\ r\simeq_r s, f) $$$

Lean4

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

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