`falsifiers_default_ok`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.ILG.Falsifiers
domain: Relativity
line: 24 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Relativity.ILG.Falsifiers on GitHub at line 24.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

falsifiers_default IndisputableMonolith.Relativity.ILG.Falsifiers
falsifiers_ok IndisputableMonolith.Relativity.ILG.Falsifiers

formal source

  21  , lensing_band := 1
  22  , gw_band := (1/1000000 : ℝ) }
  23
  24@[simp] theorem falsifiers_default_ok : falsifiers_ok falsifiers_default := by
  25  simp [falsifiers_ok, falsifiers_default]
  26  repeat' constructor <;> norm_num
  27
  28end ILG
  29end Relativity
  30end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.