abbrev
definition
def or abbrev
ComparisonOperator
show as:
view Lean formalization →
formal statement (Lean)
64abbrev ComparisonOperator := ℝ → ℝ → ℝ
proof body
Definition body.
65
66/-- The cost function derived from a comparison operator by fixing the
67second argument at the multiplicative identity. Under scale invariance,
68this is well-defined on the multiplicative group of positive ratios. -/
used by (40)
-
generatorOfLawsOfLogic -
real_supports_logic -
ContinuousCombinerAnalysisInputs -
continuous_combiner_bilinear -
continuous_combiner_bilinear_classification -
continuous_combiner_finite_smoothness_to_top -
continuous_combiner_log_smoothness_bootstrap -
ContinuousCombinerMollifierFiniteSmoothness -
ContinuousCombinerPsiAffineCompletion -
continuous_combiner_psi_affine_forcing -
ContinuousCombinerSecondDerivativeInput -
ContinuousRouteIndependence -
laws_continuous_subsumes_polynomial -
laws_polynomial_implies_continuous -
log_aczel_data_of_laws -
polynomial_implies_continuous -
RCL_is_unique_functional_form_of_logic_continuous -
SatisfiesLawsOfLogicContinuous -
derivedCost -
ExcludedMiddle -
excluded_middle_implies_continuous -
Identity -
identity_implies_normalized -
J_is_unique_cost_under_logic -
laws_of_logic_imply_dalembert_hypotheses -
NonContradiction -
non_contradiction_and_scale_imply_reciprocal -
NonTrivial -
RCL_is_unique_functional_form_of_logic -
RouteIndependence