BorderClosure.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.PermanentBorder.HasBorderDeterminant.coefficientwise_limit line 14
Source documentation
Fixed-size border representations are closed under sequential coefficientwise limits. The approximating matrices remain arbitrary complex affine matrices of exactly the original size; no uniform rate or coefficient bound is assumed.
```
theorem HasBorderDeterminant.coefficientwise_limit
    {σ : Type*} [Fintype σ] {n : ℕ} {P : ℕ → Poly σ} {p : Poly σ}
    (hP : ∀ j, HasBorderDeterminant n (P j))
    (hp : ∀ d : σ →₀ ℕ,
      Tendsto (fun j => (P j).coeff d) atTop (𝓝 (p.coeff d))) :
    HasBorderDeterminant n p := by
…
```
Mentions: OAI.PermanentBorder.Poly, OAI.PermanentBorder.HasBorderDeterminant