theorem proved term proof

`sbh_saturation_nonzero`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  76theorem sbh_saturation_nonzero (Rs : ℝ) (h_Rs : Rs > 0) :
  77    HorizonArea Rs / (4 * ell0^2) ≠ 0 :=

Term-mode proof.

  78  ne_of_gt (sbh_saturation_positive Rs h_Rs)
  79
  80end Compact
  81end Relativity
  82end IndisputableMonolith

Lean names referenced from this declaration's body.

ell0 in IndisputableMonolith.Constants decl_use
ell0 in IndisputableMonolith.Constants.Derivation decl_use
HorizonArea in IndisputableMonolith.Relativity.Compact.BlackHoleEntropy decl_use
sbh_saturation_positive in IndisputableMonolith.Relativity.Compact.BlackHoleEntropy decl_use