ContMDiffWithinAt — Mathlib

English

A closing of the equivalence: Sum.map f g is ContMDiff iff both f and g are ContMDiff; plus decomposition lemmas.

Русский

Гладкость Sum.map f g равносильна тому, что f и g гладкие; плюс раскладки.

LaTeX

$$$ ContMDiff I J n (Sum.map f g) \iff (ContMDiff I J n f \land ContMDiff I J n g) $$$

Lean4

/-- A function is `n` times continuously differentiable within a set at a point in a manifold if
it is continuous and it is `n` times continuously differentiable in this set around this point, when
read in the preferred chart at this point. -/
def ContMDiffWithinAt (n : WithTop ℕ∞) (f : M → M') (s : Set M) (x : M) :=
  LiftPropWithinAt (ContDiffWithinAtProp I I' n) f s x

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