meromorphicNFAt_inv — Mathlib

English

A simplified form of the inverse invariance: MeromorphicNFAt f⁻¹ x ↔ MeromorphicNFAt f x.

Русский

Упрощённая форма инвариантности обратного: MeromorphicNFAt f⁻¹ x ↔ MeromorphicNFAt f x.

LaTeX

$$$MeromorphicNFAt\ f^{-1}\ x \iff MeromorphicNFAt\ f\ x$$$

Lean4

/-- A function to 𝕜 is meromorphic in normal form at a point iff its inverse is.
-/
@[simp]
theorem meromorphicNFAt_inv {f : 𝕜 → 𝕜} : MeromorphicNFAt f⁻¹ x ↔ MeromorphicNFAt f x
    where
  mp := by
    nth_rw 2 [← inv_inv f]
    exact .inv
  mpr hf := by simpa using hf.inv

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