neg_iff — Mathlib

English

MeromorphicAt (-f) x is equivalent to MeromorphicAt f x (simplicity of negation).

Русский

Мероморфность (-f) в x эквивалентна мероморфности f в x (упрощение через отрицание).

LaTeX

$$$MeromorphicAt (-f) x \\leftrightarrow MeromorphicAt f x$$$

Lean4

@[simp]
theorem neg_iff {f : 𝕜 → E} {x : 𝕜} : MeromorphicAt (-f) x ↔ MeromorphicAt f x :=
  ⟨fun h ↦ by simpa only [neg_neg] using h.neg, MeromorphicAt.neg⟩

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