contDiffOn_of_subsingleton — Mathlib

English

If F is a subsingleton, then f is C^n on a set s (i.e., ContDiffOn 𝕜 n f s).

Русский

Если F единичен, то f гладко C^n на множестве s; т.е. ContDiffOn 𝕜 n f s.

LaTeX

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

Lean4

@[nontriviality]
theorem contDiffOn_of_subsingleton [Subsingleton F] : ContDiffOn 𝕜 n f s := by rw [Subsingleton.elim f fun _ => 0];
  exact contDiffOn_const

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