pith. machine review for the scientific record. sign in
lemma proved tactic proof

zeroWidthCert_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)

 116lemma zeroWidthCert_valid {Species : Type} (Z : Species → Int) (Fgap : Int → ℝ) :
 117    Valid Z Fgap (zeroWidthCert Z Fgap) := by

proof body

Tactic-mode proof.

 118  refine {
 119    M0_pos := by simp [zeroWidthCert]
 120  , Fgap_in := by
 121      intro i
 122      dsimp [zeroWidthCert, Igap, memI]
 123      constructor <;> linarith
 124  , Ires_in_Igap := by
 125      intro i
 126      dsimp [zeroWidthCert, Igap]
 127      constructor <;> linarith
 128  }
 129
 130/-- Exact anchor identity from a zero-width certificate. -/

depends on (15)

Lean names referenced from this declaration's body.