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

IsDynamicallyStable

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)

  78def IsDynamicallyStable (sol : TOVSolution) (P_c : ℝ) : Prop :=

proof body

Definition body.

  79  StrictMonoOn sol.M_of_Pc (Set.Iio P_c)
  80
  81/-! ## Oppenheimer-Volkoff Limit -/
  82
  83/-- **THE OPPENHEIMER-VOLKOFF LIMIT** (free neutron gas, no interactions):
  84    M_OV ≈ 0.71 M_sun.
  85
  86    This is a lower bound on the true M_TOV since nuclear interactions
  87    provide additional repulsive pressure. -/

depends on (6)

Lean names referenced from this declaration's body.