instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf

English

IsScalarTower holds for pointed ContMDiffMap fibers with a base self-model.

Русский

IsScalarTower сохраняется для указанных волокон ContMDiffMap с базовой моделью self.

LaTeX

$$$\text{IsScalarTower } 𝕜 (PointedContMDiffMap 𝕜 I M (WithTop.some instTopENat.top) x) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some instTopENat.top))$$$

Lean4

instance {x : M} : IsScalarTower 𝕜 C^∞⟮I, M; 𝕜⟯⟨x⟩ C^∞⟮I, M; 𝕜⟯ :=
  IsScalarTower.right

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