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

Identity

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)

  93def Identity (C : ComparisonOperator) : Prop :=

proof body

Definition body.

  94  ∀ x : ℝ, 0 < x → C x x = 0
  95
  96/-- **Non-contradiction (reciprocal symmetry)**: the cost of comparing x to y
  97equals the cost of comparing y to x. The mathematical counterpart of the
  98Aristotelian law ¬(A ∧ ¬A): if comparison were not single-valued under
  99reordering, the same comparison would simultaneously hold and not hold. -/

used by (40)

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

… and 10 more

depends on (15)

Lean names referenced from this declaration's body.