coeFnAddMonoidHom_injective — Mathlib

English

The map p ↦ (x ↦ p(x)) is injective on seminorms; i.e., if p ≠ q, then their functions differ somewhere.

Русский

Отображение p ↦ (x ↦ p(x)) инъективно на полунормы; то есть если p ≠ q, то их функции различаются где-то.

LaTeX

$$Injectivity of coeFnAddMonoidHom: for p ≠ q, there exists x with p(x) ≠ q(x).$$

Lean4

theorem coeFnAddMonoidHom_injective : Function.Injective (coeFnAddMonoidHom 𝕜 E) :=
  show @Function.Injective (Seminorm 𝕜 E) (E → ℝ) (↑) from DFunLike.coe_injective

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