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

rs_consistent_with_microscope

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)

 186theorem rs_consistent_with_microscope :
 187    eotvos_parameter 9.80665 9.80665 < microscope_bound := by

proof body

Term-mode proof.

 188  rw [rs_eotvos_zero]; unfold microscope_bound; norm_num
 189
 190end
 191
 192end EquivalencePrinciple
 193end Gravity
 194end IndisputableMonolith

depends on (3)

Lean names referenced from this declaration's body.