coe_injective — Mathlib

English

The injectivity of the coefficient extraction map holds for ContMDiffMap with simp tag.

Русский

Сохранено свойство инъективности отображения извлечения коэффициентов для ContMDiffMap (с пометкой simp).

LaTeX

$$$\forall {f g},\; (ContMDiffMap.instFunLike.coe f = ContMDiffMap.instFunLike.coe g) \Rightarrow f = g$$$

Lean4

theorem coe_injective ⦃f g : C^n⟮I, M; I', M'⟯⦄ (h : (f : M → M') = g) : f = g :=
  DFunLike.ext' h

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