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

anchorEq_implies_Zeq_nonneg

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)

  37lemma anchorEq_implies_Zeq_nonneg
  38  {Z' : Species → Int} (h : AnchorEq (Species:=Species) (Z:=Z) (Fgap:=Fgap) Z')

proof body

Tactic-mode proof.

  39  (h_inj : ∀ a b : ℤ, 0 ≤ a → 0 ≤ b → Fgap a = Fgap b → a = b)
  40  {i : Species} (hZnonneg : 0 ≤ Z i) (hZ'nonneg : 0 ≤ Z' i) : Z' i = Z i := by
  41  have h_eq := h i
  42  exact h_inj (Z' i) (Z i) hZ'nonneg hZnonneg h_eq
  43
  44/-- If anchor-equality held under any ablation, it would contradict the certified anchor. -/

depends on (6)

Lean names referenced from this declaration's body.