instFunLike — Mathlib

English

Two objects in the locally finite within-U setting are equal if they agree pointwise as functions.

Русский

Два элемента пространства локально конечных внутри U равны, если их значения совпадают в каждой точке.

LaTeX

$$$\\forall D_1,D_2:\\text{locallyFinsuppWithin } U Y,\\ (\\forall x, D_1(x)=D_2(x)) \\Rightarrow D_1=D_2$$$

Lean4

/-- Functions with locally finite support within `U` are `FunLike`: the coercion to functions is
injective.
-/
instance [Zero Y] : FunLike (locallyFinsuppWithin U Y) X Y
    where
  coe D := D.toFun
  coe_injective' := fun ⟨_, _, _⟩ ⟨_, _, _⟩ ↦ by simp

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