Alphabeta Math
CorollaryStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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.

The content of a compact Jordan image is the integral of the absolute Jacobian determinant

Statement

Under the hypotheses of Change of variables for an injective C1C^1 map on a compact Jordan set, cont⁡(g(K))=∫K∣det⁡Dg(x)∣ dx.\operatorname{cont}(g(K))=\int_K|\det Dg(x)|\,dx.

Facts & Assumptions

Given: Open UU, injective C1C^1 map gg with invertible derivative, and compact Jordan K⊆UK\subseteq U.

[L1]

Compact-Jordan change of variables applies to every bounded integrable function on g(K)g(K) (Change of variables for an injective C1C^1 map on a compact Jordan set).

[L2]

The integral of the constant-one function over a Jordan set is its Jordan content (A bounded set is Jordan measurable iff its indicator is Riemann integrable, and the integral is its Jordan content).

Proof

technique · direct
1.1

By [L1], g(K)g(K) is Jordan and change of variables applies to the constant function 11 on it.

L1given
2.1

Its pullback is ∣det⁡Dg∣|\det Dg|, while [L2] identifies the image integral with cont⁡(g(K))\operatorname{cont}(g(K)). This is the displayed formula.

L1L2step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 109 results over 22 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