Continuity at the next time endpoint

The zero trace used at each step of lem:bu-iterate follows from vanishing on the preceding open time interval and continuity up to the endpoint.

theorem ESS.bu_zero_at_time_of_left (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hcont : ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1)) (τ : ℝ) (hτ : 0 < τ) (hτ1 : τ < 1) (hzero : ∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → ∀ (t : ℝ), 0 < t → t < τ → w (x, t) = 0) (x : CKN.Foundation.Parabolic.Vec3) (hx : 0 < x 2) : w (x, τ) = 0

Vanishing on every earlier positive time implies vanishing at a time strictly inside the half-space cylinder.