English
A function f is conservative on a region U if for every rectangle lying inside U, the wedge integral along the rectangle is antisymmetric: wedgeIntegral(z,w,f) = - wedgeIntegral(w,z,f).
Русский
Функция f консервативна на области U, если для каждого прямоугольника внутри U интеграл по ромбовидной траектории равен противоположному интегралу по обращённой траектории.
LaTeX
$$$\\operatorname{IsConservativeOn}(f,U) \\iff \\forall z,w,\\; \\; \\text{Rectangle}(z,w) \\subseteq U \\Rightarrow \\operatorname{wedgeIntegral}(z,w,f) = -\\operatorname{wedgeIntegral}(w,z,f).$$$
Lean4
/-- A function `f` `IsConservativeOn` in `U` if, for any rectangle contained in `U`
the integral of `f` over the rectangle is zero. -/
def IsConservativeOn (f : ℂ → E) (U : Set ℂ) : Prop :=
∀ z w, Rectangle z w ⊆ U → wedgeIntegral z w f = -wedgeIntegral w z f
