fun_inv

Mathlib.Analysis.Meromorphic.Basic

URI: https://scilib.ai/kg/mathlib#MeromorphicAt.fun_inv

English

MeromorphicAt f⁻¹ x is equivalent to MeromorphicAt f x (simplicity of inversion).

Русский

MeromorphicAt f⁻¹ x эквивалентно MeromorphicAt f x (упрощение через инверсию).

LaTeX

$$$MeromorphicAt f^{-1} x \\leftrightarrow MeromorphicAt f x$$$

Lean4

@[fun_prop]
theorem fun_inv {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) : MeromorphicAt (fun z ↦ (f z)⁻¹) x :=
  hf.inv

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

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

Разделы

Аффилиация

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