Keyword: divisible

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

Definition Cake Valuation formalized

Theorem Chooser Is Always Envy-Free staged

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

Theorem Cut-and-Choose Is Envy-Free at a Fair Cut staged

Theorem Cut-and-Choose Output Is a Complete Partition staged

Theorem Cutter Does Not Envy at a Fair Cut staged

Definition Divisible Allocation formalized

Definition Divisible Cardinal Instance formalized

Definition Divisible Envy-Free, Proportional, Equitable Predicates formalized

Definition Divisible Measure Instance formalized

Definition Divisible Ordinal Instance formalized

Lemma Dubins–Spanier Inductive Step staged

Theorem Dubins–Spanier Proportional Existence staged

Theorem Dubins–Spanier as a Rule on Measure Instances staged

Theorem EF + Proportional Existence (Stromquist Corollary) staged

Theorem EF ⇒ Proportional (Measure Valuations) staged

Theorem Envy-Free Existence (Stromquist, n Agents) staged

Lemma Fair Assignment from a Common KKM Point staged

Theorem Fair Cut Point Exists staged

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

Definition Measure Valuation formalized

Theorem Measure-Instance EF ↔ Real-Valued Cardinal EF staged

Theorem Measure-Instance Existence Wrappers staged

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

Lemma Normalized Measure Valuation ↔ Probability Measure staged

Lemma Piece-Value Function Is Continuous on the Division Simplex staged

Theorem Proportional Existence on [0,1] (n Agents) staged

Definition Stromquist Agent-Preference Union U(i) formalized

Definition Stromquist Pieces from the Division Simplex formalized

Definition Stromquist Preference Sets A(i, j) formalized

Definition Stromquist Shifted-Cell Approximation staged

Definition Stromquist Unique-Preference Sets B(i, j) formalized

Theorem Stromquist — Unusual Case (Shifted-Cell Limit) staged

Theorem Stromquist — Usual Case (U Covers the Simplex) staged

Theorem Two-Agent EF Existence via Cut-and-Choose staged