coe_injective' — Mathlib

English

The coercion toContinuousMap is injective: if toContinuousMap f = toContinuousMap g then f = g (in the appropriate sense).

Русский

Приведение к непрерывной карте инъективно: если toContinuousMap f = toContinuousMap g, то f = g.

LaTeX

$$Injective (toContinuousMap : F → C(X,Y))$$

Lean4

/-- Coercion to a `ContinuousMap` is injective.

The unprimed version `ContinuousMap.coe_injective`
is used for the coercion from `C(X, Y)` to `X → Y`. -/
protected theorem coe_injective' {F : Type*} [FunLike F X Y] [ContinuousMapClass F X Y] :
    Injective (toContinuousMap : F → C(X, Y)) :=
  .of_comp (f := DFunLike.coe) DFunLike.coe_injective

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