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

ZeroWindingCert

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)

 123structure ZeroWindingCert where
 124  center : ℂ
 125  radius : ℝ
 126  radius_pos : 0 < radius
 127  cert : ComplexCarrierCert
 128  cert_match : cert.center = center ∧ cert.radius = radius
 129  zero_winding : ∀ (r : ℝ), 0 < r → r < radius →
 130    contourWinding cert r = 0
 131
 132/-- Extract a `ZeroWindingCert` from a `ComplexCarrierCert`. -/
 133def ComplexCarrierCert.toZeroWindingCert (cert : ComplexCarrierCert) :
 134    ZeroWindingCert where
 135  center := cert.center

proof body

Definition body.

 136  radius := cert.radius
 137  radius_pos := cert.radius_pos
 138  cert := cert
 139  cert_match := ⟨rfl, rfl⟩
 140  zero_winding := carrier_zero_winding cert
 141
 142/-- The Euler carrier's zero-winding certificate for any σ₀ > 1/2. -/

used by (16)

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

depends on (4)

Lean names referenced from this declaration's body.