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

nonTrivial_iff_distinguishability

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)

  82theorem nonTrivial_iff_distinguishability
  83    (C : ComparisonOperator) (hSI : ScaleInvariant C) :
  84    NonTrivial C ↔ Distinguishability C :=

proof body

Term-mode proof.

  85  ⟨distinguishability_of_nonTrivial C, nonTrivial_of_distinguishability C hSI⟩
  86
  87/-! ## A canonical form of `SatisfiesLawsOfLogic` using distinguishability -/
  88
  89/-- The canonical Aristotelian form of the Law of Logic, with
  90distinguishability replacing the algebraic non-triviality predicate. -/

depends on (18)

Lean names referenced from this declaration's body.