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

Valid

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)

  49structure Valid {Species : Type} (Z : Species → Int) (Fgap : Int → ℝ) (C : AnchorCert Species) : Prop where
  50  M0_pos : 0 < C.M0.lo
  51  Fgap_in : ∀ i : Species, memI (Igap C (Z i)) (Fgap (Z i))
  52  Ires_in_Igap : ∀ i : Species,
  53    (Igap C (Z i)).lo ≤ (C.Ires i).lo ∧ (C.Ires i).hi ≤ (Igap C (Z i)).hi
  54

used by (12)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.