Keyword: cake-cutting

Lemma CDF of a Non-Atomic Finite Measure on ℝ Is Continuous staged

Definition Cake Valuation formalized

Definition Cut-and-Choose Allocation and Fair Cut Point formalized

Definition Divisible Allocation formalized

Lemma IVT — Cut Point Exists for Non-Atomic Measures on [0,1] staged

Definition Measure Valuation formalized

Lemma Non-Atomicity Is Preserved by Subtype.val Pushforward staged