inv — Mathlib

English

Meromorphic in normal form is preserved under taking inverses.

Русский

Сохранение мероморфности в нормальной форме выполняется при взятии обратной функции.

LaTeX

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

Lean4

/-- If `f` is meromorphic in normal form, then so is its inverse.
-/
theorem inv {f : 𝕜 → 𝕜} (hf : MeromorphicNFAt f x) : MeromorphicNFAt f⁻¹ x :=
  by
  rcases hf with h | ⟨n, g, h₁, h₂, h₃⟩
  · left
    filter_upwards [h] with x hx
    simp [hx]
  · right
    use -n, g⁻¹, h₁.inv h₂, (by simp_all)
    filter_upwards [h₃] with y hy
    simp only [Pi.inv_apply, hy, Pi.smul_apply', Pi.pow_apply, smul_eq_mul, mul_inv_rev, zpow_neg]
    ring

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