contMDiff_of_discreteTopology — Mathlib

English

If M has discrete topology, every function f: M → M' is C^n (hence ContMDiff).

Русский

Если топология пространства M дискретна, любая функция f: M → M' является C^n (и ContMDiff).

LaTeX

$$$[DiscreteTopology M]\Rightarrow ContMDiff I I' n f$$$

Lean4

theorem contMDiff_of_discreteTopology [DiscreteTopology M] : ContMDiff I I' n f :=
  by
  intro x
  apply contMDiff_const (c := f x).contMDiffAt.congr_of_eventuallyEq
  simp [EventuallyEq]

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