`anchorIdentity_of_zeroWidthCert`

proved

show as: view math explainer →

module: IndisputableMonolith.Recognition.Certification
domain: Recognition
line: 131 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Recognition.Certification on GitHub at line 131.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 128  }
 129
 130/-- Exact anchor identity from a zero-width certificate. -/
 131lemma anchorIdentity_of_zeroWidthCert {Species : Type} (Z : Species → Int) (Fgap : Int → ℝ)
 132    (res : Species → ℝ) (hres : ∀ i, memI ((zeroWidthCert Z Fgap).Ires i) (res i)) :
 133  ∀ i : Species, res i = Fgap (Z i) := by
 134  intro i
 135  have h := hres i
 136  dsimp [zeroWidthCert, memI] at h
 137  exact le_antisymm h.2 h.1
 138
 139end
 140
 141end Certification
 142end Recognition
 143end IndisputableMonolith

papers checked against this theorem

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