When I was reading Ziegler's book "Lectures on Polytopes" this statement appeared to be never proven formally.
Question: does every (convex, bounded, non-empty) polytope have a facet?
Here I assume that the polytope $P\subset\Bbb R^d$ has dimensions $d$, and a facet is a face of dimension $d-1$.
Depending on the amount of theory developed to this point there are many ways to prove this. But it seems some element in the chain towards such a proof it missing in the book. E.g, proving any of the following statements might already be sufficient:
- the face lattice is graded of length $d+1$ (stated but never proven in Ziegler)
- the face lattice is co-atomic (proven using duality and the next unproven fact)
- given a $\delta$-face $f$ of $P$, its dual face in $P^\circ$ is of dimension $d-1-\delta$ (not proven as far as I can tell)
Maybe I am just overlooking the proof in the book, but an elementary self-contained proof of the existence of a facet is welcome anyway.
I am not familiar with Ziegler's book and will be using Grunbaum as a reference. That is, I define a face of a convex set to be its intersection with a supporting hyperplane, and a facet to be a maximal proper face.
Let us prove that every polyhedron $P$ has a facet. Let $\mathcal{H}:=\{H_i\}_{i=1}^n$ be an irredundant family of hyperplanes such that $P:=\cap_{i=1}^nH_i^+$, where $H_i^+$ is the positive closed half-space defined by $H_i$. Then every $H_i$ is a supporting hyperplane for $P$. By definition, $P\cap H_1$ is a face of $P$. Additionally, since $\mathcal{H}$ is irredundant, $P\cap H_1$ has codimension $1$, i.e. $aff(P\cap H_1)=H_1$.
Let $P\cap H$ be another proper face of $P$. Suppose that $P\cap H_1\subseteq P\cap H$. Then, $$P\cap H_1\subseteq H\Rightarrow aff(P\cap H_1)\subseteq H\Rightarrow H_1\subseteq H\Rightarrow H_1=H\Rightarrow P\cap H_1=P\cap H.$$ Therefore, $P\cap H_1$ is a facet.