`existenceUniquenessCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.ExistenceUniquenessFromCost
domain: Foundation
line: 67 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.ExistenceUniquenessFromCost on GitHub at line 67.

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

  64  isolated : ∀ {x : ℝ}, 0 < x → x ≠ 1 → 0 < Jcost x
  65
  66/-- Existence uniqueness certificate. -/
  67def existenceUniquenessCert : ExistenceUniquenessCert where
  68  zero_iff_one := @cost_zero_set_singleton
  69  unique_member := @cost_zero_set_has_one_member
  70  log_symmetric := @jcost_log_symmetric
  71  isolated := @jcost_isolated_from_zero
  72
  73end
  74end ExistenceUniquenessFromCost
  75end Foundation
  76end IndisputableMonolith

papers checked against this theorem

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