LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Shared boundary arcs cancel when finitely many elementary regions are glued

Statement

Let $D = D_{1} \cup \dots \cup D_{N}$ be a finite elementary Green region with its supplied decomposition, and let $G$ be a continuous planar vector field on a neighbourhood of $D$ . Then

$\sum_{ℓ = 1}^{N} \int_{\partial D_{ℓ}} G \cdot d r = \int_{\partial D} G \cdot d r .$

If $H : D \to R$ is continuous, then $H$ is integrable over $D$ and

$\sum_{ℓ = 1}^{N} \iint_{D_{ℓ}} H d A = \iint_{D} H d A .$

Facts & Assumptions

Given: The nonempty finite decomposition and fields in the Statement.

[L1]

The pieces have pairwise disjoint interiors; each positive-length internal arc belongs to exactly two pieces with opposite induced orientations, and pairwise intersections are finite unions of complete boundary arcs and endpoints (Type I, Type II, and elementary regions for Green's theorem).

[L2]

The positive boundary chain of the union is obtained by deleting both copies of every shared internal arc and retaining all surviving oriented arcs; the boundary integral over a chain is the finite sum of the integrals over its arcs, and each piece's own positive boundary integral is likewise the sum over its four arcs (Positive orientation of elementary-region boundaries).

[L3]

Vector line integrals add under concatenation and negate under reversal (Line integrals under reversal and concatenation).

[L4]

A continuous graph over a compact nondegenerate rectangle has content zero; content-zero sets pass to subsets, and finite unions are content zero by combining their finite covers (The graph of a continuous function on a closed nondegenerate rectangle in $R^{m}$ has content zero in $R^{m + 1}$ , Measure zero and content zero in $R^{m}$ by countable and finite cube covers).

[L5]

A bounded function on a rectangle is Riemann integrable exactly when its discontinuity set is null. A bounded set is Jordan measurable exactly when its boundary has content zero, and the indicator of a Jordan set is integrable with integral equal to its content (Lebesgue's criterion in $R^{m}$ : a bounded function on a closed nondegenerate rectangle is Riemann integrable iff its discontinuity set is null, A bounded set in $R^{m}$ is Jordan measurable iff its boundary is null, equivalently of content zero, A bounded set is Jordan measurable iff its indicator is Riemann integrable, and the integral is its Jordan content).

[L6]

Integration over a Jordan set is integration of its zero extension to a bounding rectangle, and multidimensional integrals are linear, monotone, and satisfy $∣ \int f ∣ \leq \int ∣ f ∣$ (The Riemann integral of a bounded function over a bounded Jordan measurable set, Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ ).

[L7]

A continuous real function on a nonempty compact metric space is bounded and attains a maximum and a minimum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[L8]

A closed bounded real interval is compact, continuous images of compact sets are compact, compact subsets of metric spaces are closed and bounded, and closed bounded subsets of $R^{2}$ are compact (A subset of $R$ is compact if and only if it is closed and bounded, The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset, A compact subset of a metric space is closed and bounded, Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

Proof

technique · direct

1.1

In the sum of the piece-boundary line integrals, each shared positive-length arc occurs once in each orientation by [L1]. Its two contributions cancel by [L3]. Arc endpoints are merely partition points and create no additional line-integral term.

givenL1L3

1.2

Choose one rectangle containing all pieces. Each piece boundary is a finite union of continuous graph arcs and endpoints. Their parameter intervals are compact, so [L8] makes every arc closed and bounded. The finite union $S : = ⋃_{ℓ = 1}^{N} \partial D_{ℓ}$ is therefore closed and bounded, hence compact by [L8]. By [L4], $S$ has content zero. The boundary of $D$ and every multiple-membership point lie in $S$ .

givenL1L4L8algebra

2.1

By [L2] each side is a finite sum over oriented arcs: the left side sums over the arcs of every piece boundary, and the right side sums over the arcs surviving deletion. Step 1.1 pairs off exactly the deleted arcs, and each such pair contributes zero, so the two finite sums are equal. This is a rearrangement of finitely many reals and needs no single closed path, so it holds whether or not $D$ is connected or simply connected. For $N = 1$ there are no internal arcs and the two lists coincide.

step 1.1L2L3

2.2

By [L7], $H$ is bounded on the nonempty compact set $D$ ; fix $M \geq 0$ with $∣ H ∣ \leq M$ there, so every zero extension below is bounded by $M$ . The zero extension of $H ∣_{D_{ℓ}}$ is continuous away from $\partial D_{ℓ}$ , and the zero extension of $H$ from $D$ is continuous away from $\partial D$ . Their discontinuity sets are therefore subsets of $S$ , which is null by [L4]. Hence [L5] makes all these extensions integrable. By [L6], these are precisely the indicated region integrals.

step 1.2L4L5L6L7

3.1

With $M$ as in step 2.2, let $q$ be the sum of the piecewise zero extensions minus the zero extension from $D$ . It is integrable by [L6] and vanishes outside the set of multiple-membership points, hence outside $S$ ; at a point of $S$ at most $N$ piece extensions and the extension from $D$ are nonzero, so $∣ q ∣ \leq (N + 1) M 1_{S}$ . Since $S$ is closed, its boundary is contained in $S$ and has content zero by step 1.2; [L5] therefore makes $S$ Jordan measurable with content $0$ . Thus [L5] and [L6] give $∣ \int q ∣ \leq (N + 1) M \int 1_{S} = 0.$

step 1.2step 2.2L5L6algebra

4.1

Thus $\int q = 0$ . Expanding $q$ with linearity in [L6] gives the second displayed equality.

step 3.1L6algebra∎

Depends on

Used by

Green's theorem for finite unions of elementary regions Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 196 results over 30 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Lebl, Basic Analysis II, section 10.6 (standard reference, not scraped)