pith. machine review for the scientific record. sign in
theorem proved term proof

divFree_of_forall

show as:
view Lean formalization →

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)

1201theorem divFree_of_forall {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1202    (hDF : ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2, divConstraint k ((extendByZero (H.uN N t)) k) = 0) :
1203    IsDivergenceFreeTraj HC.u := by

proof body

Term-mode proof.

1204  intro t k
1205  exact divConstraint_eq_zero_of_forall (HC := HC) (t := t) (k := k) (hDF := fun N => hDF N t k)
1206
1207/-- Mild Stokes/heat identity passes to the limit under modewise convergence,
1208assuming it holds for every approximant (modewise, for `t ≥ 0`). -/

used by (1)

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

depends on (12)

Lean names referenced from this declaration's body.