neg

Mathlib.Analysis.Analytic.Constructions

URI: https://scilib.ai/kg/mathlib#AnalyticAt.neg

English

The negation equivalence is a simplification rule for analytic at.

Русский

Эквивалентность аналитичности при отрицании является упрощением для аналитичности в точке.

LaTeX

$$$analyticAt\\, 𝕜( -f )\\; x \\iff \\ analyticAt\\, 𝕜 f x$$$

Lean4

@[fun_prop]
theorem neg (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (-f) x :=
  hf.fun_neg

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

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

Разделы

Аффилиация

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