instIsManifoldMinSmoothnessOfNatWithTopENat_1

English

Jacobi/Leibniz identities hold for vector field Lie brackets on manifolds.

Русский

Идентичности Якоби/Лейбница справедливы для скобок Ли векторных полей на многообразиях.

LaTeX

$$$[U, [V, W]] = [[U, V], W] + [V, [U, W]]$$$

Lean4

instance [IsManifold I (minSmoothness 𝕜 2) M] : IsManifold I (minSmoothness 𝕜 1) M :=
  IsManifold.of_le (n := minSmoothness 𝕜 2) (minSmoothness_monotone (by norm_cast))

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