No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
70private theorem LE_strictMono (m : ℕ) : StrictMono (LE f c R hf m) :=
proof body
Term-mode proof.
71 (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
72 (fun n => hf (CE f c R hf m n) (m + 1))).choose_spec.choose_spec.1
73
used by (4)
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
depends on (3)
Lean names referenced from this declaration's body.
-
bounded_subseq_tendsto
in IndisputableMonolith.NavierStokes.FourierExtraction
decl_use
-
CE
in IndisputableMonolith.NavierStokes.FourierExtraction
decl_use
-
LE
in IndisputableMonolith.NavierStokes.FourierExtraction
decl_use