congr — Mathlib

English

If f is meromorphic on U, g agrees with f on U, and U is open, then g is meromorphic on U.

Русский

Если f мероморфна на U, а g совпадает с f на U и U открыто, то g мероморфна на U.

LaTeX

$$$\text{MeromorphicOn}(f, U) \Rightarrow (\text{Set.EqOn}(f, g, U) \land \text{IsOpen}(U)) \Rightarrow \text{MeromorphicOn}(g, U)$$$

Lean4

theorem congr (h_eq : Set.EqOn f g U) (hu : IsOpen U) : MeromorphicOn g U :=
  by
  refine fun x hx ↦ (hf x hx).congr (EventuallyEq.filter_mono ?_ nhdsWithin_le_nhds)
  exact eventually_of_mem (hu.mem_nhds hx) h_eq

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