English
The normal form on U equals the original function on U if and only if the original function already has a normal form on U.
Русский
Нормальная форма на U равна исходной функции на U тогда и только тогда, когда сама функция уже имеет нормальную форму на U.
LaTeX
$$$toMeromorphicNFOn\ f\ U = f \iff MeromorphicNFOn\ f\ U$$
Lean4
/-- If `f` has normal form on `U`, then `f` equals `toMeromorphicNFOn f U`.
-/
@[simp]
theorem toMeromorphicNFOn_eq_self : toMeromorphicNFOn f U = f ↔ MeromorphicNFOn f U :=
by
constructor <;> intro h
· rw [h.symm]
apply meromorphicNFOn_toMeromorphicNFOn
· ext x
by_cases hx : x ∈ U
· simp only [toMeromorphicNFOn, h.meromorphicOn, ↓reduceDIte, hx]
rw [toMeromorphicNFAt_eq_self.2 (h hx)]
· simp [toMeromorphicNFOn, h.meromorphicOn, hx]
