theorem LoomisWhitney.sum_fiber_mul_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [DecidableEq γ] (S : Finset (α × β × γ)) : have π_αβ := Finset.image (fun (p : α × β × γ) => (p.1, p.2.1)) S; have π_αγ := Finset.image (fun (p : α × β × γ) => (p.1, p.2.2)) S; have π_βγ := Finset.image (fun (p : α × β × γ) => (p.2.1, p.2.2)) S; have f := fun (p : β × γ) => {x ∈ S | (x.2.1, x.2.2) = p}.card; have g := fun (b : β) => {q ∈ π_αβ | q.2 = b}.card; ∑ p ∈ π_βγ, f p * g p.1 ≤ π_αβ.card * π_αγ.card

Combinatorial fiber inequality used in the proof of Loomis-Whitney for $n = 3$. Writing $f(b,c)$ for the size of the fiber of the $\beta\gamma$-projection at $(b,c)$ and $g(b)$ for the size of the fiber of the $\alpha\beta$-projection at $b$, $\sum_{(b,c) \in \pi_{\beta\gamma}} f(b,c)\, g(b) \le |\pi_{\alpha\beta}| \cdot |\pi_{\alpha\gamma}|$.

theorem LoomisWhitney.loomis_whitney {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [DecidableEq γ] (S : Finset (α × β × γ)) : S.card ^ 2 ≤ (Finset.image (fun (p : α × β × γ) => (p.1, p.2.1)) S).card * (Finset.image (fun (p : α × β × γ) => (p.1, p.2.2)) S).card * (Finset.image (fun (p : α × β × γ) => (p.2.1, p.2.2)) S).card

Corollary 10.4.6 (discrete Loomis-Whitney for $n = 3$). For any finite set $S \subseteq \alpha \times \beta \times \gamma$, $$ |S|^2 \le |\pi_{\alpha\beta}(S)| \cdot |\pi_{\alpha\gamma}(S)| \cdot |\pi_{\beta\gamma}(S)|, $$ where $\pi_{ij}$ denotes the coordinate projection.

theorem LoomisWhitney.loomis_whitney_continuous (S : Set (ℝ × ℝ × ℝ)) (hS : MeasurableSet S) : MeasureTheory.volume S ^ 2 ≤ MeasureTheory.volume ((fun (p : ℝ × ℝ × ℝ) => (p.1, p.2.1)) '' S) * MeasureTheory.volume ((fun (p : ℝ × ℝ × ℝ) => (p.1, p.2.2)) '' S) * MeasureTheory.volume (Prod.snd '' S)

Continuous Loomis-Whitney for $\mathbb{R}^3$ (Corollary 10.4.6, measure-theoretic form): for a measurable set $S \subseteq \mathbb{R}^3$, $\mathrm{vol}(S)^2 \le \prod_{i=1}^{3} \mathrm{vol}_2(\pi_i(S))$, where $\pi_i$ is the projection forgetting the $i$-th coordinate.