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

no_feasible_if_angle_below_threshold

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)

  47theorem no_feasible_if_angle_below_threshold
  48    {x y z : R3} {Amax : ℝ} (hθlt : angleAt x y z < thetaMin Amax)
  49    (p : EightTickParams) : ∀ n : ℤ, ¬ feasible x y z Amax p n := by

proof body

Term-mode proof.

  50  intro n h
  51  have : angleAt x y z ≥ thetaMin Amax := h.left
  52  exact (not_le.mpr hθlt) this
  53
  54/-- If a geometric threshold holds and there exists a permitted time slot,
  55then a feasible event exists. -/

depends on (8)

Lean names referenced from this declaration's body.