smooth_functions_tower — Mathlib

English

There is a canonical algebra structure on the fiber C^∞⟮I, M; 𝕜⟯⟨x⟩ over each x ∈ M.

Русский

Существуют канонические алгебраические структуры на волокне C^∞⟮I, M; 𝕜⟯⟨x⟩ над каждым x ∈ M.

LaTeX

$$$\;\forall x: M,\; \text{Algebra } (PointedContMDiffMap 𝕜 I M (WithTop.some instTopENat.top) x)\; (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some instTopENat.top))$$$

Lean4

instance smooth_functions_tower : IsScalarTower 𝕜 C^∞⟮I, M; 𝕜⟯ C^∞⟮I, M; 𝕜⟯ := by infer_instance

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