coe_fn_injective — Mathlib

English

The map e ↦ EquivLike.toFunLike.coe e is injective: if two Equivs have the same underlying function, they are equal.

Русский

Отображение e ↦ EquivLike.toFunLike.coe e инъективно: если два эквивалентных отображения имеют одну и ту же функциональную составляющую, они равны.

LaTeX

$$$\\forall e_1,e_2:\\alpha \\to \\beta,\\; (e_1 = e_2) \\\\Rightarrow (\\operatorname{toFunLike}(e_1) = \\operatorname{toFunLike}(e_2)).$$$

Lean4

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

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