English
Differentials respect composition of maps: 𝒅(g ∘ f) x = (𝒅g(f x)) ∘ 𝒅f x.
Русский
Дифференциалы сохраняют композицию: 𝒅(g ∘ f) x = (𝒅g(f x)) ∘ 𝒅f x.
LaTeX
$$$$ 𝒅(g \circ f) x = (𝒅 g (f x)) \circ (𝒅 f x). $$$$
Lean4
/-- Infinitely differentiable diffeomorphism between `M` and `M'` with respect to `I` and `I'`. -/
@[scoped term_parser 1000]
public meta def «term_≃ₘ⟮_,_⟯_» : Lean.TrailingParserDescr✝ :=
ParserDescr.trailingNode✝ `Manifold.«term_≃ₘ⟮_,_⟯_» 1022 0
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ≃ₘ⟮") (ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "⟯ "))
(ParserDescr.cat✝ `term 0))
