contDiff_of_subsingleton — Mathlib

English

If the target type F is a singleton (subsingleton), then any function f: E → F is C^n for every n.

Русский

Если целевой тип F является одиночным, то любая функция f: E → F является C^n для любого порядка n.

LaTeX

$$$ [\text{Subsingleton } F] \Rightarrow \operatorname{ContDiff}_{\mathbb{K}}^{n}(f) $$$

Lean4

@[nontriviality]
theorem contDiff_of_subsingleton [Subsingleton F] : ContDiff 𝕜 n f := by rw [Subsingleton.elim f fun _ => 0];
  exact contDiff_const

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