IncomingSpanning.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Incoming spanning inside a cochain interval, used to force an empty placement.

theorem OAI.HarmonicArtin.ParabolicIntersections.incoming_spanning_step line 16
Source documentation
If the next higher layer is absent, exactness expresses every basis vector through incoming arrows in the same layer. Iterated path images record this statement without losing possible linear cancellations.
```
theorem incoming_spanning_step (E : BasedComplex Q (K := ℂ) I) (hE : E.IsMinimal Q)
…
```