instAlgebraSomeENatTopContMDiffMapModelWithCornersSelf

English

Alternative algebra instance on pointed C^∞ maps with modelWithCornersSelf.

Русский

Альтернативный экземпляр алгебры на указанных C^∞ отображениях с моделью-with-corners Self.

LaTeX

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

Lean4

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

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