feat(MeasureTheory): prove the TFAE characterizations of Jordan measurability - #666

Open

Chessing234 wants to merge 3 commits into

teorth:mainfrom

Chessing234:measure-jordan-equiv

Commits on Aug 25, 2026

feat(MeasureTheory): prove the TFAE characterizations of Jordan measurability
Chessing234
committed
8123d5c
fix(MeasureTheory): prove the symmetric-difference subset by cases
Chessing234
committed
645b200
fix(MeasureTheory): use Set.diff_union_inter in the TFAE decomposition
Chessing234
committed
7193d0b