29def LocalSection {M : Type} [TopologicalSpace M] (S : RecognitionSheaf M) (U : Set M) : Type :=
proof body
Definition body.
30 { f : U → ℝ // ∀ x : U, f x = S.potential x } 31 32/-- The J-cost derivative at the unit ratio. 33 Since J(1) = 0 is the global minimum, J'(1) = 0. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.