coeFn_injective — Mathlib

English

Two C^n-diffeomorphisms are equal if they agree on all inputs; i.e., extensionality holds for Diffeomorph.

Русский

Два диффеоморфизма класса C^n равны, если они совпадают на всех точках; то есть существует принцип экстенсивности для Diffeomorph.

LaTeX

$$$\forall x\; (h(x) = h'(x)) \Rightarrow h = h'.$$$

Lean4

/-- Coercion to function `fun h : M ≃ₘ^n⟮I, I'⟯ M' ↦ (h : M → M')` is injective. -/
theorem coeFn_injective : Injective ((↑) : (M ≃ₘ^n⟮I, I'⟯ M') → (M → M')) :=
  DFunLike.coe_injective

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