theorem Gallery.chambers_ne_nil {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} (g : Gallery K) : g.chambers ≠ []

The chamber list of a gallery is nonempty.

theorem Gallery.last_mem_of_connects {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} {g : Gallery K} {C D : Finset V} (hconn : g.Connects C D) : D ∈ g.chambers

If $g$ connects $C$ to $D$, then $D$ appears in the chamber list of $g$.

theorem Gallery.gallery_concat {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} (C₁ C₂ C₃ : Finset V) (g₁ g₂ : Gallery K) (hconn₁ : g₁.Connects C₁ C₂) (hconn₂ : g₂.Connects C₂ C₃) : ∃ (g₃ : Gallery K), g₃.Connects C₁ C₃ ∧ g₃.length = g₁.length + g₂.length ∧ C₂ ∈ g₃.chambers

Gallery concatenation: galleries $g_1 : C_1 \rightsquigarrow C_2$ and $g_2 : C_2 \rightsquigarrow C_3$ combine into a gallery $g_3 : C_1 \rightsquigarrow C_3$ with $\ell(g_3) = \ell(g_1) + \ell(g_2)$ and $C_2 \in g_3$.