pith. machine review for the scientific record. sign in
structure definition def or abbrev

JCostComparative

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)

 192structure JCostComparative (L : Type*) [RSConfigSpace L] where
 193  /-- The J-cost function -/
 194  J : L → L → ℝ
 195  /-- J(ℓ, ℓ) = 0 -/
 196  self_zero : ∀ ℓ, J ℓ ℓ = 0
 197  /-- J ≥ 0 -/
 198  nonneg : ∀ ℓ₁ ℓ₂, 0 ≤ J ℓ₁ ℓ₂
 199  /-- Symmetry (for undirected version) -/
 200  symm : ∀ ℓ₁ ℓ₂, J ℓ₁ ℓ₂ = J ℓ₂ ℓ₁
 201  /-- Triangle inequality -/
 202  triangle : ∀ ℓ₁ ℓ₂ ℓ₃, J ℓ₁ ℓ₃ ≤ J ℓ₁ ℓ₂ + J ℓ₂ ℓ₃
 203
 204/-- J-cost gives a recognition distance -/

used by (2)

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

depends on (7)

Lean names referenced from this declaration's body.