theorem proved term proof

`failureMode_injective`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 217theorem failureMode_injective : Function.Injective failureMode := by

Term-mode proof.

 218  intro a b h
 219  cases a <;> cases b <;> simp [failureMode] at h ⊢
 220

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

falsifierRegistryCert in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use

Lean names referenced from this declaration's body.

failureMode in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use