pith. machine review for the scientific record. sign in
theorem proved tactic proof

forced_of_scalar_uniqueness

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  21theorem forced_of_scalar_uniqueness {n : ℕ}
  22    (F : Vec n → ℝ) (α : Vec n) (G : ℝ → ℝ)
  23    (hfactor : ∀ x : Vec n, F x = G (aggregate α x))
  24    (hscalar : ∀ {u : ℝ}, 0 < u → G u = Jcost u) :
  25    ∀ x : Vec n, F x = JcostN α x := by

proof body

Tactic-mode proof.

  26  intro x
  27  calc
  28    F x = G (aggregate α x) := hfactor x
  29    _ = Jcost (aggregate α x) := hscalar (aggregate_pos α x)
  30    _ = JcostN α x := by simp [JcostN_eq_Jcost_aggregate]
  31
  32/-- Existential version of the forcing theorem. -/

used by (1)

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

depends on (17)

Lean names referenced from this declaration's body.