comp — Mathlib

English

A function is conformal at x iff its derivative is a conformal map.

Русский

Функция конформна в точке x тогда и только тогда, когда её производная в x конформна.

LaTeX

$$$\\operatorname{ConformalAt}(f,x) \\iff \\operatorname{IsConformalMap}(fderiv_\\mathbb{R} f x)$$$

Lean4

theorem comp {f : X → Y} {g : Y → Z} (hf : Conformal f) (hg : Conformal g) : Conformal (g ∘ f) := fun x =>
  (hg <| f x).comp x (hf x)

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