Keyword: efx

Theorem EF ⇒ EFX (Monotone Valuations) staged

Theorem EFX Existence — 2 Agents, 2 Goods staged

Theorem EFX Existence — Two Agents, Any Finite Good Set staged

Theorem EFX from No-Envy + Monotonicity staged

Lemma EFX from a Singleton-Bundle Sufficient Condition staged

Definition EFX — Envy-Free Up to Any Good formalized

Theorem EFX ⇒ EF1 staged