63structure MultiplicativeRecognizer (𝒞 : Type*) where 64 /-- The underlying geometric recognizer onto positive reals. -/ 65 recognizer : Recognizer 𝒞 {x : ℝ // 0 < x} 66 /-- The continuous comparison operator on positive reals. -/ 67 comparator : ComparisonOperator 68 /-- The comparator satisfies the Law of Logic (all four Aristotelian 69 conditions plus scale invariance and non-triviality). -/ 70 laws : SatisfiesLawsOfLogic comparator 71 72namespace MultiplicativeRecognizer 73 74variable {𝒞 : Type*} 75 76/-- The cost function induced by a multiplicative recognizer: the derived 77cost of its comparator on positive ratios. -/
used by (11)
From the project-wide theorem graph. These declarations reference this one in their body.