differentiableAt

Mathlib.Analysis.Calculus.Conformal.NormedSpace

URI: https://scilib.ai/kg/mathlib#ConformalAt.differentiableAt

English

If f is conformal at x, then f is differentiable at x.

Русский

Если f конформна в x, то она дифференцируема в x.

LaTeX

$$$\\operatorname{ConformalAt}(f,x) \\Rightarrow \\operatorname{DifferentiableAt}(\\mathbb{R}, f, x)$$$

Lean4

theorem differentiableAt {f : X → Y} {x : X} (h : ConformalAt f x) : DifferentiableAt ℝ f x :=
  let ⟨_, h₁, _⟩ := h
  h₁.differentiableAt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru