pith. machine review for the scientific record. sign in
def definition def or abbrev

H_MLUncertaintyIsDiscrete

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)

 243def H_MLUncertaintyIsDiscrete (ML : ℝ) : Prop :=

proof body

Definition body.

 244  100 ≤ ML ∧ ML ≤ 550 →
 245    ∃ n : ℤ, n ∈ Set.Icc 10 13 ∧
 246    ML = phi_power n -- SCAFFOLD
 247
 248/-- The uncertainty in M/L is discrete. -/

depends on (9)

Lean names referenced from this declaration's body.