coeFn_mk — Mathlib

English

If two bundled C^n maps have equal underlying functions, then the two maps are equal.

Русский

Если две упакованные C^n карты имеют одинаковые базовые функции, то они равны друг другу.

LaTeX

$$$\forall {f,g: C^n⟮I, M; I', M'⟯},\; (f : M \to M') = g \Rightarrow f = g$$$

Lean4

@[simp]
theorem coeFn_mk (f : M → M') (hf : ContMDiff I I' n f) : DFunLike.coe (F := C^n⟮I, M; I', M'⟯) ⟨f, hf⟩ = f :=
  rfl

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