Aggregation bundle: this chapter has no def material of its own (3/3 decls are node theorems). The namespace is declared ...

import Mathlib
import Definitions.Def_ChapterFriedrichsExtension
import Definitions.Def_ChapterSirkRitzSpectrum

/-!
# Chapter FriedrichsFormGap — the Friedrichs form gap

Aggregation bundle: this chapter has no def material of its own (3/3 decls are
node theorems).  The namespace is declared so the dot-named thm stubs' `open`
resolves; the statements' names come from the imported upstream def bundles
(FriedrichsExtension, SirkRitzSpectrum).
-/

noncomputable section

namespace BookProof.FriedrichsFormGap

end BookProof.FriedrichsFormGap