theorem other other

`CE_succ`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  68private theorem CE_succ (m : ℕ) : CE f c R hf (m + 1) = CE f c R hf m ∘ LE f c R hf m := rfl

From the project-wide theorem graph. These declarations reference this one in their body.

CE_conv_le in IndisputableMonolith.NavierStokes.FourierExtraction decl_use
CE_factor in IndisputableMonolith.NavierStokes.FourierExtraction decl_use
CE_strictMono in IndisputableMonolith.NavierStokes.FourierExtraction decl_use
D_succ_gt in IndisputableMonolith.NavierStokes.FourierExtraction decl_use

Lean names referenced from this declaration's body.