conformalAt — Mathlib

English

If X is a subsingleton, every map f: X → Y is conformal at every x ∈ X.

Русский

Если X — единичное множество, любая функция f: X → Y конформна в каждой точке x ∈ X.

LaTeX

$$$\\text{If } X\\text{ is a singleton and } f:X\\to Y, \\; \\operatorname{ConformalAt}(f,x)\\text{ for any } x \\in X$$$

Lean4

@[nontriviality]
theorem conformalAt [Subsingleton X] (f : X → Y) (x : X) : ConformalAt f x :=
  ⟨0, hasFDerivAt_of_subsingleton _ _, isConformalMap_of_subsingleton _⟩

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