toMeromorphicNFOn — Mathlib

English

A simplified form: MeromorphicNFAt of inverse is equivalent to MeromorphicNFAt of the original.

Русский

Упрощенная форма: мероморфность при обратном равносильна мероморфности исходной.

LaTeX

$$$MeromorphicNFAt\ (Pi.instInv.inv f)\ x \iff MeromorphicNFAt\ f\ x$$$

Lean4

/-- If `f` is meromorphic on `U`, convert `f` to normal form on `U` by changing its
values along a discrete subset within `U`. Otherwise, returns the 0 function.
-/
noncomputable def toMeromorphicNFOn : 𝕜 → E :=
  by
  by_cases h₁f : MeromorphicOn f U
  · intro z
    by_cases hz : z ∈ U
    · exact toMeromorphicNFAt f z z
    · exact f z
  · exact 0

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