inv_iff

Mathlib.Analysis.Meromorphic.Basic

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

← MathLib Explorer

English

If f is meromorphic at x, then f⁻¹ is meromorphic at x.

Русский

Если f мероморфна в x, то f⁻¹ мероморфна в x.

LaTeX

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

Lean4

@[simp]
theorem inv_iff {f : 𝕜 → 𝕜} {x : 𝕜} : MeromorphicAt f⁻¹ x ↔ MeromorphicAt f x :=
  ⟨fun h ↦ by simpa only [inv_inv] using h.inv, MeromorphicAt.inv⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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