def definition def or abbrev

`Distinguishability`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  43def Distinguishability (C : ComparisonOperator) : Prop :=

proof body

Definition body.

  44  ∃ x y : ℝ, 0 < x ∧ 0 < y ∧ C x y ≠ 0
  45
  46/-- **Equivalence (forward)**: distinguishability implies the algebraic
  47non-triviality predicate, given Scale Invariance. -/

used by (11)

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

ScaleInvariantOn in IndisputableMonolith.Foundation.DomainBootstrap decl_use
constZero_not_distinguishable in IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability decl_use
distinguishability_of_absoluteFloor in IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability decl_use
distinguishability_of_nonTrivial in IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability decl_use
nonTrivial_iff_distinguishability in IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability decl_use
nonTrivial_of_distinguishability in IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability decl_use
SatisfiesLawsOfLogicCanonical in IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability decl_use
meta_principle_status in IndisputableMonolith.Meta.Axioms decl_use
pillar2_information_monotonicity in IndisputableMonolith.RecogGeom.Foundations decl_use
Distinguishable in IndisputableMonolith.RecogGeom.Indistinguishable decl_use
localResolution_covers in IndisputableMonolith.RecogGeom.Indistinguishable decl_use

depends on (1)

Lean names referenced from this declaration's body.

ComparisonOperator in IndisputableMonolith.Foundation.LogicAsFunctionalEquation decl_use