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

fringe_frequency_grounded

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)

 128theorem fringe_frequency_grounded (tau0 : ℝ) (h_tau0 : tau0 > 0) :
 129    ShadowFringeFrequency tau0 > 0 := by

proof body

Term-mode proof.

 130  unfold ShadowFringeFrequency
 131  positivity
 132
 133end Lensing
 134end Relativity
 135end IndisputableMonolith

depends on (4)

Lean names referenced from this declaration's body.