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)
41class GWObservationalFacts : Prop where
42 gw170817_bound : |c_T_squared_RS - 1| < 1e-15
43
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (2)
Lean names referenced from this declaration's body.
-
gw170817_bound
in IndisputableMonolith.Relativity.GW.Constraints
decl_use
-
c_T_squared_RS
in IndisputableMonolith.Relativity.GW.PropagationSpeed
decl_use