const_smul

Mathlib.Analysis.Calculus.Conformal.NormedSpace

URI: https://scilib.ai/kg/mathlib#Conformal.const_smul

English

If c ≠ 0, then the map x ↦ c · f(x) is conformal at x.

Русский

Если c ≠ 0, отображение x ↦ c · f(x) конформно в x.

LaTeX

$$$\\operatorname{ConformalAt}(x \\mapsto c \\cdot f(x), x)$$$

Lean4

theorem const_smul {f : X → Y} (hf : Conformal f) {c : ℝ} (hc : c ≠ 0) : Conformal (c • f) := fun x =>
  (hf x).const_smul hc

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

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

Разделы

Аффилиация

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