IsExactOn — Mathlib

English

If U ⊆ V and f is conservative on V, then f is conservative on U.

Русский

Если U ⊆ V и f консервативна на V, то она консервативна и на U.

LaTeX

$$$\\text{If } U \\subseteq V \\text{ and } \\operatorname{IsConservativeOn}(f,V), \\text{ then } \\operatorname{IsConservativeOn}(f,U).$$$

Lean4

/-- A function `f` `IsExactOn` in `U` if it is the complex derivative of a function on `U`.

In complex variable theory, this is also referred to as "having a primitive". -/
def IsExactOn (f : ℂ → E) (U : Set ℂ) : Prop :=
  ∃ g, ∀ z ∈ U, HasDerivAt g (f z) z

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