contMDiff_const — Mathlib

English

The constant map from any charted space to a fixed value is smooth of any finite level n.

Русский

Постоянное отображение между шарированными пространствами гладко любой заданной степени n.

LaTeX

$$$$ \forall c, \; \text{Const}_c \in C^n(M,N) \; \text{for all } n. $$$$

Lean4

theorem contMDiff_const : ContMDiff I I' n fun _ : M => c :=
  by
  intro x
  refine ⟨continuousWithinAt_const, ?_⟩
  simp only [ContDiffWithinAtProp, Function.comp_def]
  exact contDiffWithinAt_const

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