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

finite_logical_to_truth_evaluable

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)

  34theorem finite_logical_to_truth_evaluable
  35    (C : ComparisonOperator)
  36    (h : FiniteLogicalComparison C) :
  37    TruthEvaluableComparison C where
  38  self_evaluable := h.identity

proof body

Term-mode proof.

  39  reorder_single_valued := h.non_contradiction
  40  determinate_continuous := h.totality
  41  composite_determinate := counted_once_to_finite_pairwise_polynomial C h.counted_once_algebra
  42  scale_free := h.scale_invariant
  43  nontrivial := h.nontrivial
  44
  45/-- Finite logical comparison is operative positive-ratio comparison. -/

depends on (12)

Lean names referenced from this declaration's body.