structure
ChamberComplex.ThinFoldingProperties
{V : Type u_1}
[DecidableEq V]
(K : ChamberComplex V)
:
Thin folding propagation property: in a thin chamber complex, if two foldings $f, g$ agree on the image of a chamber $C$ (with both pinning a common adjacent pair), then they agree on the image of any adjacent chamber — i.e. agreement on images propagates along adjacency.
- agree_propagates_adj (f g : K.Folding) (C C' : Finset V) : K.IsMaximal C → K.IsMaximal C' → C ≠ C' → Finset.image f.morph.toFun C = C → Finset.image f.morph.toFun C' = C → Finset.image g.morph.toFun C = C → Finset.image g.morph.toFun C' = C → ∀ (E D : Finset V), K.IsMaximal E → K.IsMaximal D → K.Adjacent E D → Finset.image f.morph.toFun E = Finset.image g.morph.toFun E → Finset.image f.morph.toFun D = Finset.image g.morph.toFun D