analyticAt_neg

Mathlib.Analysis.Analytic.Constructions

URI: https://scilib.ai/kg/mathlib#analyticAt_neg

English

Inline simp lemma relating analytic of negation to original.

Русский

Упрощение аналитичности через отрицание для исходной функции.

LaTeX

$$$\\text{analyticAt\\_neg\_simp}$$$

Lean4

@[simp]
theorem analyticAt_neg : AnalyticAt 𝕜 (-f) x ↔ AnalyticAt 𝕜 f x
    where
  mp hf := by simpa using hf.neg
  mpr := .neg

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

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

Разделы

Аффилиация

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