English
Alternative instance for algebra on pointed C^∞ maps with model with corners self.
Русский
Альтернативный экземпляр для алгебры указанных C^∞ отображений с моделью с краями саму себя.
LaTeX
$$$\text{Algebra } (PointedContMDiffMap 𝕜 I M (WithTop.some instTopENat.top) x) \;\text{ over }\; (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 (WithTop.some instTopENat.top))$$$
Lean4
@[scoped macro Derivation.«termC^_⟮_,_;_⟯⟨_⟩»]
public meta def «_aux_Mathlib_Geometry_Manifold_DerivationBundle___macroRules_Derivation_termC^_⟮_,_;_⟯⟨_⟩_1» :
Macro✝ := fun
| `(C^$n⟮$I, $M; $𝕜⟯⟨$x⟩) => ``(PointedContMDiffMap $𝕜 $I $M $n $x)
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
