pith. machine review for the scientific record. sign in
structure definition def or abbrev

AsteroidTrajectoryShapingCert

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)

  89structure AsteroidTrajectoryShapingCert where
  90  carrier_band : (8.05 : ℝ) < carrier_frequency ∧ carrier_frequency < 8.10
  91  impulse_pos : 0 < impulseCoefficient
  92  deflection_zero : deflection 0 = 0
  93  deflection_nonneg : ∀ t, 0 ≤ deflection t
  94  deflection_double : ∀ t, deflection (2 * t) = 4 * deflection t
  95  deflection_pos : ∀ {t : ℝ}, t ≠ 0 → 0 < deflection t
  96

used by (1)

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

depends on (9)

Lean names referenced from this declaration's body.