def definition def or abbrev

`isMinimizer`

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

formal statement (Lean)

  61def isMinimizer (S : StrainFunctional State) (x : State) : Prop :=

Definition body.

  62  ∀ y, S.weaklyBetter x y
  63
  64/-- For non-negative strain, equilibria are minimizers. -/

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

isBalanced in IndisputableMonolith.RRF.Core.Glossary decl_use
isMinimizer in IndisputableMonolith.RRF.Core.Glossary decl_use
equilibria_are_minimizers in IndisputableMonolith.RRF.Core.Strain decl_use
exp_preserves_argmin in IndisputableMonolith.RRF.Models.Quadratic decl_use
quadratic1D_minimizer in IndisputableMonolith.RRF.Models.Quadratic decl_use
shifted_is_minimizer in IndisputableMonolith.RRF.Models.Quadratic decl_use
trivial_is_minimizer in IndisputableMonolith.RRF.Models.Trivial decl_use
equilibria_minimal in IndisputableMonolith.RRF.Theorems.OrderPreservation decl_use

Lean names referenced from this declaration's body.