divisor_restrict — Mathlib

English

Restriction of the divisor to a subset V ⊆ U commutes with restriction of the function.

Русский

Ограничение делителя к подмножеству V ⊆ U совпадает с ограничением функции.

LaTeX

$$$\text{divisor}(f, U)\rvert_V = \text{divisor}(f, V)$ for MeromorphicOn f U with V ⊆ U$$

Lean4

/-- Taking the divisor of a meromorphic function commutes with restriction.
-/
@[simp]
theorem divisor_restrict {f : 𝕜 → E} {V : Set 𝕜} (hf : MeromorphicOn f U) (hV : V ⊆ U) :
    (divisor f U).restrict hV = divisor f V := by
  ext x
  by_cases hx : x ∈ V
  · rw [Function.locallyFinsuppWithin.restrict_apply]
    simp [hf, hx, hf.mono_set hV, hV hx]
  · simp [hx]

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