meromorphicNFOn_inv — Mathlib

English

A meromorphic-in-normal-form function has its inverse meromorphic-in-normal-form as well.

Русский

Обратная функция мероморфна в нормальной форме, если сама функция мероморфна в нормальной форме.

LaTeX

$$$MeromorphicNFOn\ f^{-1} U \iff MeromorphicNFOn\ f U$$$

Lean4

/-- A function to 𝕜 is meromorphic in normal form on `U` iff its inverse is.
-/
theorem meromorphicNFOn_inv {f : 𝕜 → 𝕜} : MeromorphicNFOn f⁻¹ U ↔ MeromorphicNFOn f U
    where
  mp h _ hx := meromorphicNFAt_inv.1 (h hx)
  mpr h _ hx := meromorphicNFAt_inv.2 (h hx)

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