def
definition
def or abbrev
post_orthogonality_plateau
show as:
view Lean formalization →
formal statement (Lean)
129def post_orthogonality_plateau : Prop :=
proof body
Definition body.
130 ∀ theta : ℝ, Real.pi / 2 ≤ theta → theta ≤ Real.pi →
131 rate_action theta ≤ rate_action (Real.pi / 2) + 1
132
133/-! ## Certificate -/
134