def definition def or abbrev

`costFirstExistenceCert`

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

formal statement (Lean)

  99def costFirstExistenceCert : CostFirstExistenceCert where
 100  rsExists_iff := @rsExists_iff_one

proof body

Definition body.

 101  non_existence_costly := @non_existence_has_positive_cost
 102  nothing_diverges := divergence_at_zero_direction
 103
 104end
 105end CostFirstExistence
 106end Foundation
 107end IndisputableMonolith

depends on (4)

Lean names referenced from this declaration's body.

CostFirstExistenceCert in IndisputableMonolith.Foundation.CostFirstExistence decl_use
divergence_at_zero_direction in IndisputableMonolith.Foundation.CostFirstExistence decl_use
non_existence_has_positive_cost in IndisputableMonolith.Foundation.CostFirstExistence decl_use
rsExists_iff_one in IndisputableMonolith.Foundation.CostFirstExistence decl_use