(T T' : F →L[ℂ] F) (b : HilbertBasis ℕ ℂ F) {eps : ℝ} (hd : ‖T - T'‖ ≤ eps) (hgap : 2 * eps < minmaxGap T) : ∀ᶠ m : ℕ in atTop, 0 < minmaxLevelIn T' (galerkinSpan b m) 1

Initializing...

(T T' : F →L[ℂ] F) (b : HilbertBasis ℕ ℂ F) {eps : ℝ} (hd : ‖T - T'‖ ≤ eps) (hgap : 2 * eps < minmaxGap T) : ∀ᶠ m : ℕ in atTop, 0 < minmaxLevelIn T' (galerkinSpan b m) 1 - minmaxLevelIn T'... · Prove2Me