The Lean 4 theorem `restrictToTop_apply` in the `ChapterNavierStokesFlow` chapter of the timepiece formalization
ProvedBookProof.NavierStokesFlow.restrictToTop_applytimepiece
The Lean 4 theorem restrictToTop_apply in the ChapterNavierStokesFlow chapter of the timepiece formalization.
Preamble
-- Generated from ChapterNavierStokesFlow.lean — theorem BookProof.NavierStokesFlow.restrictToTop_apply
import Mathlib
import Definitions.Def_ChapterNavierStokesFlow
open BookProof.NavierStokesFlow
open scoped BigOperators Matrix Kronecker ComplexOrder TensorProduct
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]Formal statement
theorem BookProof.NavierStokesFlow.restrictToTop_apply (H : F →ₗ[ℂ] F) (v : (⊤ : Submodule ℂ F)) :
(restrictToTop H v : F) = H (v : F) := by sorrySource