def
definition
def or abbrev
substitutivity_forces_factorization
show as:
view Lean formalization →
formal statement (Lean)
57def substitutivity_forces_factorization
58 (J : ℝ → ℝ) (hJ0 : J 1 = 0)
59 (hSym : ∀ x : ℝ, 0 < x → J x = J x⁻¹)
60 (P : ℝ → ℝ → ℝ)
61 (hComp : ∀ x y : ℝ, 0 < x → 0 < y →
62 J (x * y) + J (x / y) = P (J x) (J y)) :
63 ContextualSubstitutivity J :=
proof body
Definition body.
64 ⟨P, hComp⟩
65
66/-- Symmetry of the combiner follows from commutativity of `(ℝ₊, ×)`:
67`J(xy) + J(x/y) = J(yx) + J(y/x)` because `xy = yx` and
68`J(x/y) = J(y/x)` by reciprocal symmetry. -/