Alphabeta Math
CorollaryStatement: Literature-sourcedProof: Literature-sourcedprecheck 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 C1 map on a compact Jordan set, cont⁡(g(K))=∫K∣det⁡Dg(x)∣ dx.

Facts & Assumptions

Given: Open U, injective C1 map g with invertible derivative, and compact Jordan K⊆U.

[L1]

Compact-Jordan change of variables applies to every bounded integrable function on g(K) (Change of variables for an injective C1 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) is Jordan and change of variables applies to the constant function 1 on it.

L1given
2.1

Its pullback is ∣det⁡Dg∣, while [L2] identifies the image integral with 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 · two levels

25 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources