theorem proved term proof

`denseDomain_nonempty`

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

formal statement (Lean)

  54theorem denseDomain_nonempty : denseDomain.Nonempty := ⟨0, trivial⟩

Term-mode proof.

  55
  56/-- The dense domain contains every finitely-supported state. -/

Lean names referenced from this declaration's body.

contains in IndisputableMonolith.Ethics.StakeGraph decl_use
denseDomain in IndisputableMonolith.NumberTheory.CostOperatorRegularity decl_use
contains in IndisputableMonolith.Numerics.Interval.Basic decl_use