SerpentineInfiniteArray.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite serpentine remains embedded after continuing its last column vertically to infinity.

lemma OAI.SLEExactGauge.Serpentine.array_normal_terminal line 14
lemma OAI.SLEExactGauge.Serpentine.array_normal_finite_terminal_disjoint line 24
theorem OAI.SLEExactGauge.Serpentine.array_normal_injective_infinite line 57
Source documentation
The complete upward-continued array is embedded on the whole closed width-one normal strip.
```
theorem array_normal_injective_infinite {m : ℕ} (hm : 0 < m) :
    InjOn (normalRibbon (arraySpine m (2 * m)) (arrayTangent m (2 * m)))
      {z : ℂ | 0 ≤ z.re ∧ |z.im| ≤ 1} := by
…
```
Mentions: OAI.SLEExactGauge.Serpentine.normalRibbon, OAI.SLEExactGauge.Serpentine.arraySpine, OAI.SLEExactGauge.Serpentine.arrayTangent